let a, b, c, d, e, f, g, h be Real; for F being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & e < f & a <= e & f <= b & F is being_homeomorphism & F . a = c & F . b = d & g = F . e & h = F . f holds
F .: [.e,f.] = [.g,h.]
let F be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ( a < b & c < d & e < f & a <= e & f <= b & F is being_homeomorphism & F . a = c & F . b = d & g = F . e & h = F . f implies F .: [.e,f.] = [.g,h.] )
assume that
A1:
a < b
and
A2:
c < d
and
A3:
e < f
and
A4:
a <= e
and
A5:
f <= b
and
A6:
F is being_homeomorphism
and
A7:
( F . a = c & F . b = d )
and
A8:
g = F . e
and
A9:
h = F . f
; F .: [.e,f.] = [.g,h.]
a <= f
by A3, A4, XXREAL_0:2;
then
f in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) }
by A5;
then A10:
f in [.a,b.]
by RCOMP_1:def 1;
then
f in the carrier of (Closed-Interval-TSpace (a,b))
by A1, TOPMETR:18;
then
h in the carrier of (Closed-Interval-TSpace (c,d))
by A9, FUNCT_2:5;
then A11:
h in [.c,d.]
by A2, TOPMETR:18;
e <= b
by A3, A5, XXREAL_0:2;
then
e in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) }
by A4;
then A12:
e in [.a,b.]
by RCOMP_1:def 1;
then
e in the carrier of (Closed-Interval-TSpace (a,b))
by A1, TOPMETR:18;
then
g in the carrier of (Closed-Interval-TSpace (c,d))
by A8, FUNCT_2:5;
then
g in [.c,d.]
by A2, TOPMETR:18;
then
[.g,h.] c= [.c,d.]
by A11, XXREAL_2:def 12;
then A13:
[.g,h.] c= the carrier of (Closed-Interval-TSpace (c,d))
by A2, TOPMETR:18;
A14:
( F is continuous & F is one-to-one )
by A6, TOPS_2:def 5;
A15:
[.g,h.] c= F .: [.e,f.]
proof
let aa be
object ;
TARSKI:def 3 ( not aa in [.g,h.] or aa in F .: [.e,f.] )
A16:
F is
one-to-one
by A6, TOPS_2:def 5;
assume
aa in [.g,h.]
;
aa in F .: [.e,f.]
then
aa in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) }
by RCOMP_1:def 1;
then consider l being
Real such that A17:
aa = l
and A18:
g <= l
and A19:
l <= h
;
A20:
rng F = [#] (Closed-Interval-TSpace (c,d))
by A6, TOPS_2:def 5;
l in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) }
by A18, A19;
then A21:
l in [.g,h.]
by RCOMP_1:def 1;
reconsider x =
(F ") . l as
Real ;
F is
onto
by A20, FUNCT_2:def 3;
then A22:
x = (F ") . l
by A16, TOPS_2:def 4;
then A23:
x in dom F
by A13, A16, A20, A21, FUNCT_1:32;
dom F = [#] (Closed-Interval-TSpace (a,b))
by A6, TOPS_2:def 5;
then reconsider e9 =
e,
f9 =
f,
x9 =
x as
Point of
(Closed-Interval-TSpace (a,b)) by A1, A12, A10, A13, A16, A20, A21, A22, FUNCT_1:32, TOPMETR:18;
reconsider g9 =
F . e9,
h9 =
F . f9,
l9 =
F . x9 as
Point of
(Closed-Interval-TSpace (c,d)) ;
reconsider gg =
g9,
hh =
h9,
ll =
l9 as
Real ;
A24:
x <= f
proof
assume
x > f
;
contradiction
then
ll > hh
by A1, A2, A7, A14, Th15;
hence
contradiction
by A9, A13, A19, A16, A20, A21, A22, FUNCT_1:32;
verum
end;
e <= x
proof
assume
e > x
;
contradiction
then
gg > ll
by A1, A2, A7, A14, Th15;
hence
contradiction
by A8, A13, A18, A16, A20, A21, A22, FUNCT_1:32;
verum
end;
then
x in { l1 where l1 is Real : ( e <= l1 & l1 <= f ) }
by A24;
then A25:
x in [.e,f.]
by RCOMP_1:def 1;
aa = F . x
by A13, A17, A16, A20, A21, A22, FUNCT_1:32;
hence
aa in F .: [.e,f.]
by A23, A25, FUNCT_1:def 6;
verum
end;
F .: [.e,f.] c= [.g,h.]
proof
let aa be
object ;
TARSKI:def 3 ( not aa in F .: [.e,f.] or aa in [.g,h.] )
assume
aa in F .: [.e,f.]
;
aa in [.g,h.]
then consider x being
object such that A26:
x in dom F
and A27:
x in [.e,f.]
and A28:
aa = F . x
by FUNCT_1:def 6;
x in { l where l is Real : ( e <= l & l <= f ) }
by A27, RCOMP_1:def 1;
then consider x9 being
Real such that A29:
x9 = x
and A30:
e <= x9
and A31:
x9 <= f
;
reconsider Fx =
F . x9 as
Real ;
reconsider e1 =
e,
f1 =
f,
x1 =
x9 as
Point of
(Closed-Interval-TSpace (a,b)) by A1, A12, A10, A26, A29, TOPMETR:18;
reconsider gg =
F . e1,
hh =
F . f1,
FFx =
F . x1 as
Real ;
A32:
Fx <= h
g <= Fx
then
Fx in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) }
by A32;
hence
aa in [.g,h.]
by A28, A29, RCOMP_1:def 1;
verum
end;
hence
F .: [.e,f.] = [.g,h.]
by A15; verum