let a, b, r, s be Real; ( 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 Th27;
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:62, TOPMETR:17, ZFMISC_1:96;
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
object ;
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:8;
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
object 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 3;
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:17, ZFMISC_1:96;
then consider x1,
x2 being
Element of the
carrier of
R^1 such that A6:
x = [x1,x2]
by A4, DOMAIN_1:1;
A7:
x2 in [.r,s.]
by A1, A2, A4, A6, ZFMISC_1:87;
A8:
(R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . x = R2Homeomorphism . x
by A4, FUNCT_1:47;
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:44;
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:87;
x1 = p `1
by A9, FINSEQ_1:44;
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:2; verum