let a, b, r, s be real number ; :: thesis:
assume A1: ( a <= b & r <= s ) ; :: thesis:
set C1 = Closed-Interval-TSpace a,b;
set C2 = Closed-Interval-TSpace r,s;
set TR = Trectangle a,b,r,s;
let h be Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s); :: thesis:
assume A2: h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] ; :: thesis:
reconsider S0 = [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] as non empty SubSpace of [:R^1 ,R^1 :] by BORSUK_3:25;
A3: closed_inside_of_rectangle a,b,r,s = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) } by JGRAPH_6:def 2;
A4: the carrier of (Trectangle a,b,r,s) = closed_inside_of_rectangle a,b,r,s by PRE_TOPC:29;
set p = |[a,r]|;
( |[a,r]| `1 = a & |[a,r]| `2 = r ) by EUCLID:56;
then |[a,r]| in closed_inside_of_rectangle a,b,r,s by A1, A3;
then reconsider T0 = Trectangle a,b,r,s as non empty SubSpace of TOP-REAL 2 ;
reconsider g = h as Function of S0,T0 ;
A5: g = R2Homeomorphism | S0 by A2;
g is onto

thus rng g c= the carrier of T0 ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis:
let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in the carrier of T0 ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A6: y = p and
A7: ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) by A3, A4;
A8: the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] = [:[.a,b.],[.r,s.]:] by A1, Th48;
A9: dom g = the carrier of S0 by FUNCT_2:def 1;
( p `1 in [.a,b.] & p `2 in [.r,s.] ) by A7;
then A10: [(p `1 ),(p `2 )] in dom g by A8, A9, ZFMISC_1:def 2;
then g . [(p `1 ),(p `2 )] = R2Homeomorphism . [(p `1 ),(p `2 )] by A2, FUNCT_1:72
.= |[(p `1 ),(p `2 )]| by Def2
.= y by A6, EUCLID:57 ;
hence y in rng g by A10, FUNCT_1:def 5; :: thesis:

end;

hence h is being_homeomorphism by A5, Th56, JORDAN16:13; :: thesis: