theorem Th5: :: UNIFORM3:10

for TG being TopologicalGroup
for e being Element of TG
for V being a_neighborhood of 1_ TG holds V * {e} is a_neighborhood of e