let G be BinContinuous TopaddGroup; :: thesis: for a being Element of G holds + a is Homeomorphism of G
let a be Element of G; :: thesis: + a is Homeomorphism of G
set f = + a;
thus ( dom (+ a) = [#] G & rng (+ a) = [#] G & + a is one-to-one ) by FUNCT_2:def 1, FUNCT_2:def 3; :: according to TOPS_2:def 5,TOPGRP_1:def 4 :: thesis: ( + a is continuous & (+ a) /" is continuous )
thus + a is continuous ; :: thesis: (+ a) /" is continuous
(+ a) /" = + (- a) by Th18;
hence (+ a) /" is continuous ; :: thesis: verum