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

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