let a, b, r, s be real number ; ( 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 )
; 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 ;
TARSKI:def 3 ( 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) )
A3:
( the
carrier of
(Trectangle a,b,r,s) = closed_inside_of_rectangle a,
b,
r,
s &
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, PRE_TOPC:29;
assume
y in rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):])
;
y in the carrier of (Trectangle a,b,r,s)
then consider x being
set such that A4:
x in dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):])
and A5:
(R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) . x = y
by FUNCT_1:def 5;
reconsider x =
x as
Point of
[:R^1 ,R^1 :] by A4;
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 A6:
x = [x1,x2]
by A4, DOMAIN_1:9;
A7:
x2 in [.r,s.]
by A1, A2, A4, A6, ZFMISC_1:106;
A8:
(R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) . x = R2Homeomorphism . x
by A4, 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) ;
A9:
(R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]) . x = <*x1,x2*>
by A8, A6, Def2;
then
x2 = p `2
by FINSEQ_1:61;
then A10:
(
r <= p `2 &
p `2 <= s )
by A7, XXREAL_1:1;
A11:
x1 in [.a,b.]
by A1, A2, A4, A6, ZFMISC_1:106;
x1 = p `1
by A9, FINSEQ_1:61;
then
(
a <= p `1 &
p `1 <= b )
by A11, XXREAL_1:1;
hence
y in the
carrier of
(Trectangle a,b,r,s)
by A5, A3, A10;
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; verum