let TG be TopologicalGroup; :: thesis: for e being Element of TG
for V being a_neighborhood of 1_ TG holds {e} * V is a_neighborhood of e
let e be Element of TG; :: thesis: for V being a_neighborhood of 1_ TG holds {e} * V is a_neighborhood of e
let V be a_neighborhood of 1_ TG; :: thesis: {e} * V 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: ( e * o is open & e * o c= {e} * V & e in e * o )
thus e * o is open by A1; :: thesis: ( e * o c= {e} * V & e in e * o )
thus e * o c= {e} * V :: thesis: e in e * o
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in e * o or x in {e} * V )
assume A4: x in e * o ; :: thesis: x in {e} * V
e * o c= e * V by A2, GROUP_3:5;
hence x in {e} * V by A4; :: thesis: verum
end;
e = e * (1_ TG) by GROUP_1:def 4;
hence e in e * o by A3, GROUP_2:27; :: thesis: verum
end;
hence {e} * V is a_neighborhood of e by CONNSP_2:6; :: thesis: verum