set T = (TOP-REAL 2) | R^2-unit_square;
take f = id ((TOP-REAL 2) | R^2-unit_square); :: according to TOPREAL2:def 1 :: thesis: f is being_homeomorphism
thus dom f = [#] ((TOP-REAL 2) | R^2-unit_square) by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] ((TOP-REAL 2) | R^2-unit_square) & f is one-to-one & f is continuous & f " is continuous )
thus rng f = [#] ((TOP-REAL 2) | R^2-unit_square) by RELAT_1:45; :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
then ( f is onto & f is one-to-one ) by FUNCT_2:def 3;
then A1: f " = f " by TOPS_2:def 4
.= f by FUNCT_1:45 ;
thus f is one-to-one ; :: thesis: ( f is continuous & f " is continuous )
thus f is continuous by FUNCT_2:94; :: thesis: f " is continuous
hence f " is continuous by A1; :: thesis: verum