for G being BinContinuous TopaddGroup
for a being Element of G holds + a is Homeomorphism of G