let T be TopGroup; :: thesis: ( ( for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ) implies T is TopologicalGroup )
assume A1: for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ; :: thesis: T is TopologicalGroup
A2: for a being Element of T
for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W

proof

let a be Element of T; :: thesis: for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W
let W be a_neighborhood of a " ; :: thesis: ex A being a_neighborhood of a st A " c= W
W is a_neighborhood of (1_ T) * (a ") by GROUP_1:def 4;
then consider A being a_neighborhood of 1_ T, B being a_neighborhood of a such that
A3: A * (B ") c= W by A1;
take B ; :: thesis: B " c= W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B " or x in W )
assume A4: x in B " ; :: thesis: x in W
then consider g being Element of T such that
A5: x = g " and
g in B ;
1_ T in A by CONNSP_2:4;
then (1_ T) * (g ") in A * (B ") by A4, A5;
then g " in A * (B ") by GROUP_1:def 4;
hence x in W by A3, A5; :: thesis: verum

end;

for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W

proof

let a, b be Element of T; :: thesis: for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W
let W be a_neighborhood of a * b; :: thesis: ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W
W is a_neighborhood of a * ((b ") ") ;
then consider A being a_neighborhood of a, B being a_neighborhood of b " such that
A6: A * (B ") c= W by A1;
consider B1 being a_neighborhood of b such that
A7: B1 " c= B by A2;
take A ; :: thesis: ex B being a_neighborhood of b st A * B c= W
take B1 ; :: thesis: A * B1 c= W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * B1 or x in W )
assume x in A * B1 ; :: thesis: x in W
then consider g, h being Element of T such that
A8: ( x = g * h & g in A ) and
A9: h in B1 ;
h " in B1 " by A9;
then h in B " by A7, Th7;
then x in A * (B ") by A8;
hence x in W by A6; :: thesis: verum

end;

hence T is TopologicalGroup by A2, Th37, Th39; :: thesis: verum