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