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 set ; :: 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 ; :: 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 number st r in R holds
r <= r2

proof

let r be real number ; :: 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 ext-real number ; :: 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 by XXREAL_2:def 10;
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 Th15;
{ r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } c= [.0,1.]

proof

let x be set ; :: 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, Th7, 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 Th3;
A18: S00 is convergent by A7, A12, A17, Th4, Th10;
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, Th10;
then S2 is convergent by Th9;
then lim S2 = lim S1 by Th9;
then A20: lim s1 = lim S1 by A12, Th6;
A21: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of 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 Element of NAT such that
A24: for m being Element of NAT st m >= n0 holds
dist ((S1 . m),(lim S1)) < r7 by A19, A22, TBSP_1:def 3;
for m being Element of NAT st m >= n0 holds
dist ((S00 . m),t1) < r

proof

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

end;

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

end;

A26: r2 >= upper_bound R by A10, SEQ_4:144;
then A27: 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 set ; :: 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 ; :: 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 A27;
A28: for r being real number st r in R2 holds
r >= upper_bound R

proof

let r be real number ; :: 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 ext-real number ; :: 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 A29: R2 is bounded_below by XXREAL_2:def 9;
then consider s2 being Real_Sequence such that
A30: ( s2 is non-increasing & s2 is convergent ) and
A31: rng s2 c= R2 and
A32: lim s2 = lower_bound R2 by Th16;
A33: 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 set ; :: 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
A34: ( r3 = x & upper_bound R <= r3 ) and
A35: r3 <= r2 and
f . r3 in F2 ;
r3 <= 1 by A2, A35, XXREAL_0:2;
hence x in [.0,1.] by A33, A34, XXREAL_1:1; :: thesis:

end;

then reconsider S1 = s2 as sequence of (Closed-Interval-MSpace (0,1)) by A31, Th7, XBOOLE_1:1;
reconsider S2 = s2 as sequence of RealSpace by METRIC_1:def 13;
A36: S1 is convergent by A30, Th10;
then S2 is convergent by Th9;
then lim S2 = lim S1 by Th9;
then A37: lim s2 = lim S1 by A30, Th6;
for n4 being Element of NAT holds S00 . n4 in F1

proof

let n4 be Element of NAT ; :: thesis:
dom s1 = NAT by FUNCT_2:def 1;
then s1 . n4 in rng s1 by FUNCT_1:def 3;
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; :: thesis:

end;

then lim S00 in F1 by A5, A7, A19, A17, Th2, Th4;
then A38: f . (lim s1) in F1 by A20, A18, A21, TBSP_1:def 3;
A39: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def 7;
then reconsider S00 = f * S1 as sequence of X by Th3;
dom f = the carrier of I[01] by FUNCT_2:def 1
.= the carrier of (Closed-Interval-MSpace (0,1)) by A39, 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;
A40: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of 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
A41: r7 > 0 and
A42: 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, A39, UNIFORM1:4;
consider n0 being Element of NAT such that
A43: for m being Element of NAT st m >= n0 holds
dist ((S1 . m),(lim S1)) < r7 by A36, A41, TBSP_1:def 3;
for m being Element of NAT st m >= n0 holds
dist ((S00 . m),t1) < r

proof

let m be Element of NAT ; :: thesis:
dom S00 = NAT by TBSP_1:4;
then A44: S00 . m = f . (S1 . m) by FUNCT_1:12;
assume m >= n0 ; :: thesis:
then dist ((lim S1),(S1 . m)) < r7 by A43;
hence dist ((S00 . m),t1) < r by A42, A44; :: thesis:

end;

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

end;

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

proof

let s be real number ; :: thesis:
assume A46: 0 < s ; :: thesis:

now

assume A47: for r being real number st r < (upper_bound R) + s holds
not r in R2 ; :: thesis:

now

per cases by A26, XREAL_1:48;

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

hence contradiction by A27, A46, A47, XREAL_1:29; :: thesis:

end;

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

end;

hence contradiction ; :: thesis:

end;

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

end;

then A57: upper_bound R = lower_bound R2 by A28, A29, SEQ_4:def 2;
S00 is convergent by A7, A30, A39, Th4, Th10;
then A58: f . (lim S1) = lim S00 by A40, TBSP_1:def 3;
for n4 being Element of NAT holds S00 . n4 in F2

proof

let n4 be Element of NAT ; :: thesis:
dom s2 = NAT by FUNCT_2:def 1;
then s2 . n4 in rng s2 by FUNCT_1:def 3;
then s2 . n4 in R2 by A31;
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; :: thesis:

end;

then lim S00 in F2 by A6, A7, A36, A39, Th2, Th4;
then f . (lim s1) in F1 /\ F2 by A57, A14, A38, A32, A37, A58, XBOOLE_0:def 4;
hence ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 ) by A26, A45, A14; :: thesis: