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 Th36;
consider C being open a_neighborhood of b such that
A2: C " c= B by Th38;
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 object ; :: 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