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 A1: 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 )
thus f is one-to-one ; :: thesis: ( f is continuous & f " is continuous )
thus A2: 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 A3: V is closed ; :: thesis: f " V is closed
thus f " V is closed by A3, FUNCT_2:171; :: thesis: verum

end;

f " = f

proof

thus f " = (id the carrier of ((TOP-REAL 2) | R^2-unit_square )) " by A1, TOPS_2:def 4
.= f by FUNCT_1:67 ; :: thesis: verum

end;

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