theorem Th42: :: TOPGRP_1:43
for G being BinContinuous TopGroup
for a being Element of G holds a * is Homeomorphism of G