let a, b, r, s be real number ; ( a <= b & r <= s implies for h being Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s) st h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] holds
h is being_homeomorphism )
assume A1:
( a <= b & r <= s )
; for h being Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s) st h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] holds
h is being_homeomorphism
set TR = Trectangle a,b,r,s;
A2:
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;
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, A2;
then reconsider T0 = Trectangle a,b,r,s as non empty SubSpace of TOP-REAL 2 ;
set C2 = Closed-Interval-TSpace r,s;
set C1 = Closed-Interval-TSpace a,b;
let h be Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s); ( h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] implies h is being_homeomorphism )
assume A3:
h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):]
; h is being_homeomorphism
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;
reconsider g = h as Function of S0,T0 ;
A4:
the carrier of (Trectangle a,b,r,s) = closed_inside_of_rectangle a,b,r,s
by PRE_TOPC:29;
A5:
g is onto
proof
thus
rng g c= the
carrier of
T0
;
XBOOLE_0:def 10,
FUNCT_2:def 3 the carrier of T0 c= proj2 g
let y be
set ;
TARSKI:def 3 ( not y in the carrier of T0 or y in proj2 g )
A6:
( the
carrier of
[:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] = [:[.a,b.],[.r,s.]:] &
dom g = the
carrier of
S0 )
by A1, Th48, FUNCT_2:def 1;
assume
y in the
carrier of
T0
;
y in proj2 g
then consider p being
Point of
(TOP-REAL 2) such that A7:
y = p
and A8:
(
a <= p `1 &
p `1 <= b &
r <= p `2 &
p `2 <= s )
by A2, A4;
(
p `1 in [.a,b.] &
p `2 in [.r,s.] )
by A8;
then A9:
[(p `1 ),(p `2 )] in dom g
by A6, ZFMISC_1:def 2;
then g . [(p `1 ),(p `2 )] =
R2Homeomorphism . [(p `1 ),(p `2 )]
by A3, FUNCT_1:72
.=
|[(p `1 ),(p `2 )]|
by Def2
.=
y
by A7, EUCLID:57
;
hence
y in proj2 g
by A9, FUNCT_1:def 5;
verum
end;
g = R2Homeomorphism | S0
by A3;
hence
h is being_homeomorphism
by A5, Th56, JORDAN16:13; verum