let a, b, c, d, e, f, g, h be Real; :: thesis: 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)); :: thesis: ( 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 ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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.] ; :: thesis: 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 ; :: thesis: contradiction
then ll > hh by A1, A2, A7, A14, Th15;
hence contradiction by A9, A13, A19, A16, A20, A21, A22, FUNCT_1:32; :: thesis: verum
end;
e <= x
proof
assume e > x ; :: thesis: contradiction
then gg > ll by A1, A2, A7, A14, Th15;
hence contradiction by A8, A13, A18, A16, A20, A21, A22, FUNCT_1:32; :: thesis: 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; :: thesis: verum
end;
F .: [.e,f.] c= [.g,h.]
proof
let aa be object ; :: according to TARSKI:def 3 :: thesis: ( not aa in F .: [.e,f.] or aa in [.g,h.] )
assume aa in F .: [.e,f.] ; :: thesis: 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
proof
per cases ( f = x or f <> x ) ;
suppose f = x ; :: thesis: Fx <= h
hence Fx <= h by A9, A29; :: thesis: verum
end;
end;
end;
g <= Fx
proof
per cases ( e = x or e <> x ) ;
suppose e = x ; :: thesis: g <= Fx
hence g <= Fx by A8, A29; :: thesis: verum
end;
suppose e <> x ; :: thesis: g <= Fx
then e < x9 by A29, A30, XXREAL_0:1;
then gg < FFx by A1, A2, A7, A14, Th15;
hence g <= Fx by A8; :: thesis: verum
end;
end;
end;
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; :: thesis: verum
end;
hence F .: [.e,f.] = [.g,h.] by A15; :: thesis: verum