let a, b, r, s be Real; ( 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:52;
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:21;
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:8;
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= rng g
let y be
object ;
TARSKI:def 3 ( not y in the carrier of T0 or y in rng 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, Th27, FUNCT_2:def 1;
assume
y in the
carrier of
T0
;
y in rng 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:49
.=
|[(p `1),(p `2)]|
by Def2
.=
y
by A7, EUCLID:53
;
hence
y in rng g
by A9, FUNCT_1:def 3;
verum
end;
g = R2Homeomorphism | S0
by A3;
hence
h is being_homeomorphism
by A5, Th34, JORDAN16:9; verum