let X be non empty MetrSpace; :: thesis:
let f be Function of I[01],(TopSpaceMetr X); :: thesis:
let F1, F2 be Subset of (TopSpaceMetr X); :: thesis:
let r1, r2 be Real; :: thesis:
assume that
A1: 0 <= r1 and
A2: r2 <= 1 and
A3: ( r1 <= r2 & f . r1 in F1 ) and
A4: f . r2 in F2 and
A5: F1 is closed and
A6: F2 is closed and
A7: f is continuous and
A8: F1 \/ F2 = the carrier of X ; :: thesis:
A9: r1 in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } by A3;
{ r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } ; :: thesis:
then ex r3 being Real st
( r3 = x & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;
hence x in REAL by XREAL_0:def 1; :: thesis:

end;

then reconsider R = { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } as non empty Subset of REAL by A9;
A10: for r being Real st r in R holds
r <= r2

proof

let r be Real; :: thesis:
assume r in R ; :: thesis:
then ex r3 being Real st
( r3 = r & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;
hence r <= r2 ; :: thesis:

end;

r2 is UpperBound of R

proof

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis:
assume r in R ; :: thesis:
then ex r3 being Real st
( r3 = r & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;
hence r <= r2 ; :: thesis:

end;

then A11: R is bounded_above ;
then consider s1 being Real_Sequence such that
A12: ( s1 is non-decreasing & s1 is convergent ) and
A13: rng s1 c= R and
A14: lim s1 = upper_bound R by Th11;
{ r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } c= [.0,1.]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } ; :: thesis:
then consider r3 being Real such that
A15: ( r3 = x & r1 <= r3 ) and
A16: r3 <= r2 and
f . r3 in F1 ;
r3 <= 1 by A2, A16, XXREAL_0:2;
hence x in [.0,1.] by A1, A15, XXREAL_1:1; :: thesis:

end;

then reconsider S1 = s1 as sequence of (Closed-Interval-MSpace (0,1)) by A13, Th5, XBOOLE_1:1;
A17: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def 7;
then reconsider S00 = f * S1 as sequence of X by Th2;
A18: S00 is convergent by A7, A12, A17, Th3, Th8;
dom f = the carrier of I[01] by FUNCT_2:def 1
.= the carrier of (Closed-Interval-MSpace (0,1)) by A17, TOPMETR:12 ;
then f . (lim S1) in rng f by FUNCT_1:3;
then reconsider t1 = f . (lim S1) as Point of X by TOPMETR:12;
reconsider S2 = s1 as sequence of RealSpace by METRIC_1:def 13;
A19: S1 is convergent by A12, Th8;
then S2 is convergent by Th7;
then lim S2 = lim S1 by Th7;
then A20: lim s1 = lim S1 by A12, Th4;
A21: for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r

proof

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider r7 being Real such that
A22: r7 > 0 and
A23: for w being Point of (Closed-Interval-MSpace (0,1))
for w1 being Point of X st w1 = f . w & dist ((lim S1),w) < r7 holds
dist (t1,w1) < r by A7, A17, UNIFORM1:4;
consider n0 being Nat such that
A24: for m being Nat st m >= n0 holds
dist ((S1 . m),(lim S1)) < r7 by A19, A22, TBSP_1:def 3;
for m being Nat st m >= n0 holds
dist ((S00 . m),t1) < r

proof

let m be Nat; :: thesis:
A25: m in NAT by ORDINAL1:def 12;
dom S00 = NAT by TBSP_1:4;
then A26: S00 . m = f . (S1 . m) by FUNCT_1:12, A25;
assume m >= n0 ; :: thesis:
then dist ((lim S1),(S1 . m)) < r7 by A24;
hence dist ((S00 . m),t1) < r by A23, A26; :: thesis:

end;

hence ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r ; :: thesis:

end;

A27: r2 >= upper_bound R by A10, SEQ_4:144;
then A28: r2 in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } by A4;
{ r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } ; :: thesis:
then ex r3 being Real st
( r3 = x & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;
hence x in REAL by XREAL_0:def 1; :: thesis:

end;

then reconsider R2 = { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } as non empty Subset of REAL by A28;
A29: for r being Real st r in R2 holds
r >= upper_bound R

proof

let r be Real; :: thesis:
assume r in R2 ; :: thesis:
then ex r3 being Real st
( r3 = r & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;
hence r >= upper_bound R ; :: thesis:

end;

upper_bound R is LowerBound of R2

proof

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis:
assume r in R2 ; :: thesis:
then ex r3 being Real st
( r3 = r & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;
hence upper_bound R <= r ; :: thesis:

end;

then A30: R2 is bounded_below ;
then consider s2 being Real_Sequence such that
A31: ( s2 is non-increasing & s2 is convergent ) and
A32: rng s2 c= R2 and
A33: lim s2 = lower_bound R2 by Th12;
A34: 0 <= upper_bound R by A1, A9, A11, SEQ_4:def 1;
{ r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } c= [.0,1.]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } ; :: thesis:
then consider r3 being Real such that
A35: ( r3 = x & upper_bound R <= r3 ) and
A36: r3 <= r2 and
f . r3 in F2 ;
r3 <= 1 by A2, A36, XXREAL_0:2;
hence x in [.0,1.] by A34, A35, XXREAL_1:1; :: thesis:

end;

then reconsider S1 = s2 as sequence of (Closed-Interval-MSpace (0,1)) by A32, Th5, XBOOLE_1:1;
reconsider S2 = s2 as sequence of RealSpace by METRIC_1:def 13;
A37: S1 is convergent by A31, Th8;
then S2 is convergent by Th7;
then lim S2 = lim S1 by Th7;
then A38: lim s2 = lim S1 by A31, Th4;
for n4 being Nat holds S00 . n4 in F1

proof

let n4 be Nat; :: thesis:
A39: n4 in NAT by ORDINAL1:def 12;
dom s1 = NAT by FUNCT_2:def 1;
then s1 . n4 in rng s1 by FUNCT_1:def 3, A39;
then s1 . n4 in R by A13;
then ( dom S00 = NAT & ex r3 being Real st
( r3 = s1 . n4 & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ) by TBSP_1:4;
hence S00 . n4 in F1 by FUNCT_1:12, A39; :: thesis:

end;

then lim S00 in F1 by A5, A7, A19, A17, Th1, Th3;
then A40: f . (lim s1) in F1 by A20, A18, A21, TBSP_1:def 3;
A41: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def 7;
then reconsider S00 = f * S1 as sequence of X by Th2;
dom f = the carrier of I[01] by FUNCT_2:def 1
.= the carrier of (Closed-Interval-MSpace (0,1)) by A41, TOPMETR:12 ;
then f . (lim S1) in rng f by FUNCT_1:3;
then reconsider t1 = f . (lim S1) as Point of X by TOPMETR:12;
A42: for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r

proof

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider r7 being Real such that
A43: r7 > 0 and
A44: for w being Point of (Closed-Interval-MSpace (0,1))
for w1 being Point of X st w1 = f . w & dist ((lim S1),w) < r7 holds
dist (t1,w1) < r by A7, A41, UNIFORM1:4;
consider n0 being Nat such that
A45: for m being Nat st m >= n0 holds
dist ((S1 . m),(lim S1)) < r7 by A37, A43, TBSP_1:def 3;
for m being Nat st m >= n0 holds
dist ((S00 . m),t1) < r

proof

let m be Nat; :: thesis:
A46: m in NAT by ORDINAL1:def 12;
dom S00 = NAT by TBSP_1:4;
then A47: S00 . m = f . (S1 . m) by FUNCT_1:12, A46;
assume m >= n0 ; :: thesis:
then dist ((lim S1),(S1 . m)) < r7 by A45;
hence dist ((S00 . m),t1) < r by A44, A47; :: thesis:

end;

hence ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r ; :: thesis:

end;

A48: r1 <= upper_bound R by A9, A11, SEQ_4:def 1;
for s being Real st 0 < s holds
ex r being Real st
( r in R2 & r < (upper_bound R) + s )

proof

let s be Real; :: thesis:
assume A49: 0 < s ; :: thesis:

now :: thesis:

assume A50: for r being Real st r < (upper_bound R) + s holds
not r in R2 ; :: thesis:

now :: thesis:

per cases by A27, XREAL_1:48;

case r2 - (upper_bound R) = 0 ; :: thesis:

hence contradiction by A28, A49, A50, XREAL_1:29; :: thesis:

end;

case A51: r2 - (upper_bound R) > 0 ; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence ex r being Real st
( r in R2 & r < (upper_bound R) + s ) ; :: thesis:

end;

then A60: upper_bound R = lower_bound R2 by A29, A30, SEQ_4:def 2;
S00 is convergent by A7, A31, A41, Th3, Th8;
then A61: f . (lim S1) = lim S00 by A42, TBSP_1:def 3;
for n4 being Nat holds S00 . n4 in F2

proof

let n4 be Nat; :: thesis:
A62: n4 in NAT by ORDINAL1:def 12;
dom s2 = NAT by FUNCT_2:def 1;
then s2 . n4 in rng s2 by FUNCT_1:def 3, A62;
then s2 . n4 in R2 by A32;
then ( dom S00 = NAT & ex r3 being Real st
( r3 = s2 . n4 & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ) by TBSP_1:4;
hence S00 . n4 in F2 by FUNCT_1:12, A62; :: thesis:

end;

then lim S00 in F2 by A6, A7, A37, A41, Th1, Th3;
then f . (lim s1) in F1 /\ F2 by A60, A14, A40, A33, A38, A61, XBOOLE_0:def 4;
hence ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 ) by A27, A48, A14; :: thesis: