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:71; :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
then A1: f " = (id the carrier of ((TOP-REAL 2) | R^2-unit_square)) " by TOPS_2:def 4
.= f by FUNCT_1:67 ;
thus f is one-to-one ; :: thesis: ( f is continuous & f " is continuous )
thus f is continuous :: thesis: f " is continuous

proof

let V be Subset of ((TOP-REAL 2) | R^2-unit_square); :: according to PRE_TOPC:def 12 :: thesis: ( not V is closed or f " V is closed )
assume V is closed ; :: thesis: f " V is closed
hence f " V is closed by FUNCT_2:171; :: thesis: verum

end;

hence f " is continuous by A1; :: thesis: verum