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