let G be BinContinuous TopGroup; :: 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