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 Th17;
hence (a +) /" is continuous ; :: thesis: verum