let G be UnContinuous TopGroup; :: thesis: inverse_op G is Homeomorphism of G
set f = inverse_op G;
thus ( dom (inverse_op G) = [#] G & rng (inverse_op G) = [#] G & inverse_op G is one-to-one ) by FUNCT_2:def 1, FUNCT_2:def 3; :: according to TOPS_2:def 5,TOPGRP_1:def 4 :: thesis: ( inverse_op G is continuous & (inverse_op G) /" is continuous )
thus inverse_op G is continuous by Def7; :: thesis: (inverse_op G) /" is continuous
inverse_op G = (inverse_op G) " by Th13
.= (inverse_op G) /" by TOPS_2:def 4 ;
hence (inverse_op G) /" is continuous by Def7; :: thesis: verum