An exact proof term for the current goal is (andEL (T1_space G Tg) (∃mult inv e : set, function_on mult (setprod G G) G ∧ function_on inv G G ∧ e ∈ G ∧ (∀x y z : set, x ∈ G → y ∈ G → z ∈ G → apply_fun mult (apply_fun mult (x,y),z) = apply_fun mult (x,apply_fun mult (y,z))) ∧ (∀x : set, x ∈ G → apply_fun mult (e,x) = x ∧ apply_fun mult (x,e) = x) ∧ (∀x : set, x ∈ G → apply_fun mult (x,apply_fun inv x) = e ∧ apply_fun mult (apply_fun inv x,x) = e) ∧ continuous_map (setprod G G) (product_topology G Tg G Tg) G Tg mult ∧ continuous_map G Tg G Tg inv) H).