let TG be TopologicalGroup; :: thesis: for e being Element of TG
for V being a_neighborhood of 1_ TG holds V * {e} is a_neighborhood of e
let e be Element of TG; :: thesis: for V being a_neighborhood of 1_ TG holds V * {e} is a_neighborhood of e
let V be a_neighborhood of 1_ TG; :: thesis: V * {e} is a_neighborhood of e
consider o being Subset of TG such that
A1: o is open and
A2: o c= V and
A3: 1_ TG in o by CONNSP_2:6;

now :: thesis: ( o * e is open & o * e c= V * {e} & e in o * e )

thus o * e is open by A1; :: thesis: ( o * e c= V * {e} & e in o * e )
thus o * e c= V * {e} :: thesis: e in o * e

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in o * e or x in V * {e} )
assume A4: x in o * e ; :: thesis: x in V * {e}
o * e c= V * e by A2, GROUP_3:5;
hence x in V * {e} by A4; :: thesis: verum

end;

e = (1_ TG) * e by GROUP_1:def 4;
hence e in o * e by A3, GROUP_2:28; :: thesis: verum

end;

hence V * {e} is a_neighborhood of e by CONNSP_2:6; :: thesis: verum