let a, b, r, s be real number ; :: thesis: ( a <= b & r <= s implies R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] is Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s) )
set C1 = Closed-Interval-TSpace a,b;
set C2 = Closed-Interval-TSpace r,s;
set TR = Trectangle a,b,r,s;
set h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):];
assume
( a <= b & r <= s )
; :: thesis: R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] is Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s)
then A1:
the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] = [:[.a,b.],[.r,s.]:]
by Th48;
dom R2Homeomorphism = [:the carrier of R^1 ,the carrier of R^1 :]
by Lm1, FUNCT_2:def 1;
then A2:
dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) = the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]
by A1, RELAT_1:91, TOPMETR:24, ZFMISC_1:119;
rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) c= the carrier of (Trectangle a,b,r,s)
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) or y in the carrier of (Trectangle a,b,r,s) )
assume
y in rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):])
;
:: thesis: y in the carrier of (Trectangle a,b,r,s)
then consider x being
set such that A3:
x in dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):])
and A4:
(R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) . x = y
by FUNCT_1:def 5;
A5:
the
carrier of
(Trectangle a,b,r,s) = closed_inside_of_rectangle a,
b,
r,
s
by PRE_TOPC:29;
A6:
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;
reconsider x =
x as
Point of
[:R^1 ,R^1 :] by A3;
A7:
(R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) . x = R2Homeomorphism . x
by A3, FUNCT_1:70;
then reconsider p =
(R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) . x as
Point of
(TOP-REAL 2) ;
dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) c= [:the carrier of R^1 ,the carrier of R^1 :]
by A1, A2, TOPMETR:24, ZFMISC_1:119;
then consider x1,
x2 being
Element of the
carrier of
R^1 such that A8:
x = [x1,x2]
by A3, DOMAIN_1:9;
(R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) . x = <*x1,x2*>
by A7, A8, Def2;
then A9:
(
x1 = p `1 &
x2 = p `2 )
by FINSEQ_1:61;
(
x1 in [.a,b.] &
x2 in [.r,s.] )
by A1, A2, A3, A8, ZFMISC_1:106;
then
(
a <= p `1 &
p `1 <= b &
r <= p `2 &
p `2 <= s )
by A9, XXREAL_1:1;
hence
y in the
carrier of
(Trectangle a,b,r,s)
by A4, A5, A6;
:: thesis: verum
end;
hence
R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] is Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s)
by A2, FUNCT_2:4; :: thesis: verum