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
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
A3: x = g * h and
A4: g in A and
A5: h in C " ;
consider k being Element of T such that
A6: h = k " and
k in C by A5;
g * (k " ) in A * B by A2, A4, A5, A6;
hence x in W by A1, A3, A6; :: thesis: verum