let T be TopologicalGroup; :: thesis: for a, b being Element of T
for W being a_neighborhood of a * (b " ) ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B " ) c= W
let a, b be Element of T; :: thesis: for W being a_neighborhood of a * (b " ) ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B " ) c= W
let W be a_neighborhood of a * (b " ); :: thesis: ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B " ) c= W
consider A being open a_neighborhood of a, B being open a_neighborhood of b " such that
A1: A * B c= W by Th37;
consider C being open a_neighborhood of b such that
A2: C " c= B by Th39;
take A ; :: thesis: ex B being open a_neighborhood of b st A * (B " ) c= W
take C ; :: thesis: A * (C " ) c= W
A3: A * B = { (g * h) where g, h is Element of T : ( g in A & h in B ) } by GROUP_2:def 2;
A4: A * (C " ) = { (g * h) where g, h is Element of T : ( g in A & h in C " ) } by GROUP_2:def 2;
A5: C " = { (g " ) where g is Element of T : g in C } by GROUP_2:def 1;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A * (C " ) or x in W )
assume x in A * (C " ) ; :: thesis: x in W
then consider g, h being Element of T such that
A6: ( x = g * h & g in A & h in C " ) by A4;
consider k being Element of T such that
A7: ( h = k " & k in C ) by A5, A6;
g * (k " ) in A * B by A2, A3, A6, A7;
hence x in W by A1, A6, A7; :: thesis: verum