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 A1: ( 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 ) ; :: thesis: F .: [.e,f.] = [.g,h.]
then A2: ( e <= b & a <= f ) by XXREAL_0:2;
A3: ( F is continuous & F is one-to-one ) by A1, TOPS_2:def 5;
( e in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) } & f in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) } ) by A1, A2;
then A4: ( e in [.a,b.] & f in [.a,b.] ) by RCOMP_1:def 1;
then ( e in the carrier of (Closed-Interval-TSpace a,b) & f in the carrier of (Closed-Interval-TSpace a,b) ) by A1, TOPMETR:25;
then ( g in the carrier of (Closed-Interval-TSpace c,d) & h in the carrier of (Closed-Interval-TSpace c,d) ) by A1, FUNCT_2:7;
then ( g in [.c,d.] & h in [.c,d.] ) by A1, TOPMETR:25;
then [.g,h.] c= [.c,d.] by XXREAL_2:def 12;
then A5: [.g,h.] c= the carrier of (Closed-Interval-TSpace c,d) by A1, TOPMETR:25;
F .: [.e,f.] = [.g,h.]

proof

thus F .: [.e,f.] c= [.g,h.] :: according to XBOOLE_0:def 10 :: thesis: [.g,h.] c= F .: [.e,f.]

proof

let aa be set ; :: 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 set such that
A6: ( x in dom F & x in [.e,f.] & aa = F . x ) by FUNCT_1:def 12;
x in { l where l is Real : ( e <= l & l <= f ) } by A6, RCOMP_1:def 1;
then consider x' being Real such that
A7: ( x' = x & e <= x' & x' <= f ) ;
F . x' in rng F by A6, A7, FUNCT_1:def 5;
then F . x' in [#] (Closed-Interval-TSpace c,d) ;
then A8: F . x' in [.c,d.] by A1, TOPMETR:25;
then reconsider Fx = F . x' as Real ;
reconsider e1 = e, f1 = f, x1 = x' as Point of (Closed-Interval-TSpace a,b) by A1, A4, A6, A7, TOPMETR:25;
reconsider gg = F . e1, hh = F . f1, FFx = F . x1 as Real by A1, A8;
A9: g <= Fx

proof

per cases ( e = x or e <> x ) ;

suppose e = x ; :: thesis: g <= Fx

hence g <= Fx by A1, A7; :: thesis: verum

end;

suppose e <> x ; :: thesis: g <= Fx

then e < x' by A7, XXREAL_0:1;
then gg < FFx by A1, A3, Th16;
hence g <= Fx by A1; :: thesis: verum

end;

end;

end;

Fx <= h

proof

per cases ( f = x or f <> x ) ;

suppose f = x ; :: thesis: Fx <= h

hence Fx <= h by A1, A7; :: thesis: verum

end;

suppose f <> x ; :: thesis: Fx <= h

then f > x' by A7, XXREAL_0:1;
then hh > FFx by A1, A3, Th16;
hence Fx <= h by A1; :: thesis: verum

end;

end;

end;

then Fx in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) } by A9;
hence aa in [.g,h.] by A6, A7, RCOMP_1:def 1; :: thesis: verum

end;

thus [.g,h.] c= F .: [.e,f.] :: thesis: verum

proof

let aa be set ; :: according to TARSKI:def 3 :: thesis: ( not aa in [.g,h.] or aa in F .: [.e,f.] )
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
A10: ( aa = l & g <= l & l <= h ) ;
A11: F is one-to-one by A1, TOPS_2:def 5;
A12: dom F = [#] (Closed-Interval-TSpace a,b) by A1, TOPS_2:def 5;
A13: rng F = [#] (Closed-Interval-TSpace c,d) by A1, TOPS_2:def 5;
l in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) } by A10;
then A14: l in [.g,h.] by RCOMP_1:def 1;
then l in rng F by A5, A13;
then l in dom (F " ) by A11, A13, TOPS_2:62;
then (F " ) . l in rng (F " ) by FUNCT_1:def 5;
then (F " ) . l in [#] (Closed-Interval-TSpace a,b) ;
then (F " ) . l in [.a,b.] by A1, TOPMETR:25;
then reconsider x = (F " ) . l as Real ;
A15: x = (F " ) . l by A11, A13, TOPS_2:def 4;
then A16: x in dom F by A5, A11, A13, A14, FUNCT_1:54;
reconsider e' = e, f' = f, x' = x as Point of (Closed-Interval-TSpace a,b) by A1, A4, A5, A11, A12, A13, A14, A15, FUNCT_1:54, TOPMETR:25;
reconsider g' = F . e', h' = F . f', l' = F . x' as Point of (Closed-Interval-TSpace c,d) ;
l' in the carrier of (Closed-Interval-TSpace c,d) ;
then l' in [.c,d.] by A1, TOPMETR:25;
then reconsider gg = g', hh = h', ll = l' as Real by A1;
A17: e <= x

proof

assume e > x ; :: thesis: contradiction
then gg > ll by A1, A3, Th16;
hence contradiction by A1, A5, A10, A11, A13, A14, A15, FUNCT_1:54; :: thesis: verum

end;

x <= f

proof

assume x > f ; :: thesis: contradiction
then ll > hh by A1, A3, Th16;
hence contradiction by A1, A5, A10, A11, A13, A14, A15, FUNCT_1:54; :: thesis: verum

end;

then x in { l1 where l1 is Real : ( e <= l1 & l1 <= f ) } by A17;
then A18: x in [.e,f.] by RCOMP_1:def 1;
aa = F . x by A5, A10, A11, A13, A14, A15, FUNCT_1:54;
hence aa in F .: [.e,f.] by A16, A18, FUNCT_1:def 12; :: thesis: verum

end;

end;

hence F .: [.e,f.] = [.g,h.] ; :: thesis: verum