theorem Th42: :: TOPGRP_1:43

for G being BinContinuous TopGroup
for a being Element of G holds a * is Homeomorphism of G