let G be UnContinuous TopaddGroup; :: thesis: add_inverse G is Homeomorphism of G
set f = add_inverse G;
thus ( dom (add_inverse G) = [#] G & rng (add_inverse G) = [#] G & add_inverse 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: ( add_inverse G is continuous & (add_inverse G) /" is continuous )
thus add_inverse G is continuous by Def7; :: thesis: (add_inverse G) /" is continuous
add_inverse G = (add_inverse G) " by Th13
.= (add_inverse G) /" by TOPS_2:def 4 ;
hence (add_inverse G) /" is continuous by Def7; :: thesis: verum