let X be non empty MetrSpace; :: thesis: for f being Function of I[01],(TopSpaceMetr X)

for F1, F2 being Subset of (TopSpaceMetr X)

for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds

ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 )

let f be Function of I[01],(TopSpaceMetr X); :: thesis: for F1, F2 being Subset of (TopSpaceMetr X)

for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds

ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 )

let F1, F2 be Subset of (TopSpaceMetr X); :: thesis: for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds

ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 )

let r1, r2 be Real; :: thesis: ( 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X implies ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 ) )

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: ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 )

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

A10: for r being Real st r in R holds

r <= r2

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.]

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

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

A29: for r being Real st r in R2 holds

r >= upper_bound R

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.]

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

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

for s being Real st 0 < s holds

ex r being Real st

( r in R2 & r < (upper_bound R) + s )

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

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: verum

for F1, F2 being Subset of (TopSpaceMetr X)

for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds

ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 )

let f be Function of I[01],(TopSpaceMetr X); :: thesis: for F1, F2 being Subset of (TopSpaceMetr X)

for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds

ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 )

let F1, F2 be Subset of (TopSpaceMetr X); :: thesis: for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds

ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 )

let r1, r2 be Real; :: thesis: ( 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X implies ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 ) )

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: ex r being Real st

( r1 <= r & r <= r2 & f . r in F1 /\ F2 )

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

then reconsider R = { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } as non empty Subset of REAL by A9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } or x in REAL )

assume x in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } ; :: thesis: x in REAL

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: verum

end;assume x in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } ; :: thesis: x in REAL

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: verum

A10: for r being Real st r in R holds

r <= r2

proof

r2 is UpperBound of R
let r be Real; :: thesis: ( r in R implies r <= r2 )

assume r in R ; :: thesis: r <= r2

then ex r3 being Real st

( r3 = r & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;

hence r <= r2 ; :: thesis: verum

end;assume r in R ; :: thesis: r <= r2

then ex r3 being Real st

( r3 = r & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;

hence r <= r2 ; :: thesis: verum

proof

then A11:
R is bounded_above
;
let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in R or r <= r2 )

assume r in R ; :: thesis: r <= r2

then ex r3 being Real st

( r3 = r & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;

hence r <= r2 ; :: thesis: verum

end;assume r in R ; :: thesis: r <= r2

then ex r3 being Real st

( r3 = r & r1 <= r3 & r3 <= r2 & f . r3 in F1 ) ;

hence r <= r2 ; :: thesis: verum

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

then reconsider S1 = s1 as sequence of (Closed-Interval-MSpace (0,1)) by A13, Th5, XBOOLE_1:1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } or x in [.0,1.] )

assume x in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } ; :: thesis: x in [.0,1.]

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: verum

end;assume x in { r3 where r3 is Real : ( r1 <= r3 & r3 <= r2 & f . r3 in F1 ) } ; :: thesis: x in [.0,1.]

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: verum

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

A27:
r2 >= upper_bound R
by A10, SEQ_4:144;
let r be Real; :: thesis: ( r > 0 implies ex n being Nat st

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r )

assume r > 0 ; :: thesis: ex n being Nat st

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r

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

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r ; :: thesis: verum

end;for m being Nat st m >= n holds

dist ((S00 . m),t1) < r )

assume r > 0 ; :: thesis: ex n being Nat st

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r

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

hence
ex n being Nat st
let m be Nat; :: thesis: ( m >= n0 implies dist ((S00 . m),t1) < r )

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: dist ((S00 . m),t1) < r

then dist ((lim S1),(S1 . m)) < r7 by A24;

hence dist ((S00 . m),t1) < r by A23, A26; :: thesis: verum

end;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: dist ((S00 . m),t1) < r

then dist ((lim S1),(S1 . m)) < r7 by A24;

hence dist ((S00 . m),t1) < r by A23, A26; :: thesis: verum

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r ; :: thesis: verum

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

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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } or x in REAL )

assume x in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } ; :: thesis: x in REAL

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: verum

end;assume x in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } ; :: thesis: x in REAL

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: verum

A29: for r being Real st r in R2 holds

r >= upper_bound R

proof

upper_bound R is LowerBound of R2
let r be Real; :: thesis: ( r in R2 implies r >= upper_bound R )

assume r in R2 ; :: thesis: r >= upper_bound R

then ex r3 being Real st

( r3 = r & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;

hence r >= upper_bound R ; :: thesis: verum

end;assume r in R2 ; :: thesis: r >= upper_bound R

then ex r3 being Real st

( r3 = r & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;

hence r >= upper_bound R ; :: thesis: verum

proof

then A30:
R2 is bounded_below
;
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in R2 or upper_bound R <= r )

assume r in R2 ; :: thesis: upper_bound R <= r

then ex r3 being Real st

( r3 = r & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;

hence upper_bound R <= r ; :: thesis: verum

end;assume r in R2 ; :: thesis: upper_bound R <= r

then ex r3 being Real st

( r3 = r & upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) ;

hence upper_bound R <= r ; :: thesis: verum

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

then reconsider S1 = s2 as sequence of (Closed-Interval-MSpace (0,1)) by A32, Th5, XBOOLE_1:1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } or x in [.0,1.] )

assume x in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } ; :: thesis: x in [.0,1.]

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: verum

end;assume x in { r3 where r3 is Real : ( upper_bound R <= r3 & r3 <= r2 & f . r3 in F2 ) } ; :: thesis: x in [.0,1.]

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: verum

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

then
lim S00 in F1
by A5, A7, A19, A17, Th1, Th3;
let n4 be Nat; :: thesis: S00 . n4 in F1

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: verum

end;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: verum

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

A48:
r1 <= upper_bound R
by A9, A11, SEQ_4:def 1;
let r be Real; :: thesis: ( r > 0 implies ex n being Nat st

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r )

assume r > 0 ; :: thesis: ex n being Nat st

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r

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

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r ; :: thesis: verum

end;for m being Nat st m >= n holds

dist ((S00 . m),t1) < r )

assume r > 0 ; :: thesis: ex n being Nat st

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r

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

hence
ex n being Nat st
let m be Nat; :: thesis: ( m >= n0 implies dist ((S00 . m),t1) < r )

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: dist ((S00 . m),t1) < r

then dist ((lim S1),(S1 . m)) < r7 by A45;

hence dist ((S00 . m),t1) < r by A44, A47; :: thesis: verum

end;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: dist ((S00 . m),t1) < r

then dist ((lim S1),(S1 . m)) < r7 by A45;

hence dist ((S00 . m),t1) < r by A44, A47; :: thesis: verum

for m being Nat st m >= n holds

dist ((S00 . m),t1) < r ; :: thesis: verum

for s being Real st 0 < s holds

ex r being Real st

( r in R2 & r < (upper_bound R) + s )

proof

then A60:
upper_bound R = lower_bound R2
by A29, A30, SEQ_4:def 2;
let s be Real; :: thesis: ( 0 < s implies ex r being Real st

( r in R2 & r < (upper_bound R) + s ) )

assume A49: 0 < s ; :: thesis: ex r being Real st

( r in R2 & r < (upper_bound R) + s )

( r in R2 & r < (upper_bound R) + s ) ; :: thesis: verum

end;( r in R2 & r < (upper_bound R) + s ) )

assume A49: 0 < s ; :: thesis: ex r being Real st

( r in R2 & r < (upper_bound R) + s )

now :: thesis: ex r being Real st

( r < (upper_bound R) + s & r in R2 )

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

assume A50:
for r being Real st r < (upper_bound R) + s holds

not r in R2 ; :: thesis: contradiction

end;not r in R2 ; :: thesis: contradiction

now :: thesis: ( ( r2 - (upper_bound R) = 0 & contradiction ) or ( r2 - (upper_bound R) > 0 & contradiction ) )end;

hence
contradiction
; :: thesis: verumper cases
( r2 - (upper_bound R) = 0 or r2 - (upper_bound R) > 0 )
by A27, XREAL_1:48;

end;

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

set rs0 = min ((r2 - (upper_bound R)),s);

set r0 = (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2);

A52: min ((r2 - (upper_bound R)),s) > 0 by A49, A51, XXREAL_0:21;

then A53: upper_bound R < (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by XREAL_1:29, XREAL_1:215;

min ((r2 - (upper_bound R)),s) <= r2 - (upper_bound R) by XXREAL_0:17;

then A54: (upper_bound R) + (min ((r2 - (upper_bound R)),s)) <= (upper_bound R) + (r2 - (upper_bound R)) by XREAL_1:7;

A55: (min ((r2 - (upper_bound R)),s)) / 2 < min ((r2 - (upper_bound R)),s) by A52, XREAL_1:216;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) < (upper_bound R) + (min ((r2 - (upper_bound R)),s)) by XREAL_1:8;

then A56: (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) <= r2 by A54, XXREAL_0:2;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) <= 1 by A2, XXREAL_0:2;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in the carrier of I[01] by A1, A48, A52, BORSUK_1:40, XXREAL_1:1;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in dom f by FUNCT_2:def 1;

then f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in rng f by FUNCT_1:def 3;

then f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in the carrier of (TopSpaceMetr X) ;

then f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in the carrier of X by TOPMETR:12;

then A57: ( f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in F1 or f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in F2 ) by A8, XBOOLE_0:def 3;

upper_bound R <= (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by A52, XREAL_1:29, XREAL_1:215;

then A58: r1 <= (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by A48, XXREAL_0:2;

min ((r2 - (upper_bound R)),s) <= s by XXREAL_0:17;

then (min ((r2 - (upper_bound R)),s)) / 2 < s by A55, XXREAL_0:2;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) < (upper_bound R) + s by XREAL_1:8;

then A59: not (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in R2 by A50;

upper_bound R < (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by A52, XREAL_1:29, XREAL_1:215;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in R by A59, A58, A56, A57;

hence contradiction by A11, A53, SEQ_4:def 1; :: thesis: verum

end;set r0 = (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2);

A52: min ((r2 - (upper_bound R)),s) > 0 by A49, A51, XXREAL_0:21;

then A53: upper_bound R < (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by XREAL_1:29, XREAL_1:215;

min ((r2 - (upper_bound R)),s) <= r2 - (upper_bound R) by XXREAL_0:17;

then A54: (upper_bound R) + (min ((r2 - (upper_bound R)),s)) <= (upper_bound R) + (r2 - (upper_bound R)) by XREAL_1:7;

A55: (min ((r2 - (upper_bound R)),s)) / 2 < min ((r2 - (upper_bound R)),s) by A52, XREAL_1:216;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) < (upper_bound R) + (min ((r2 - (upper_bound R)),s)) by XREAL_1:8;

then A56: (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) <= r2 by A54, XXREAL_0:2;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) <= 1 by A2, XXREAL_0:2;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in the carrier of I[01] by A1, A48, A52, BORSUK_1:40, XXREAL_1:1;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in dom f by FUNCT_2:def 1;

then f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in rng f by FUNCT_1:def 3;

then f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in the carrier of (TopSpaceMetr X) ;

then f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in the carrier of X by TOPMETR:12;

then A57: ( f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in F1 or f . ((upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2)) in F2 ) by A8, XBOOLE_0:def 3;

upper_bound R <= (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by A52, XREAL_1:29, XREAL_1:215;

then A58: r1 <= (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by A48, XXREAL_0:2;

min ((r2 - (upper_bound R)),s) <= s by XXREAL_0:17;

then (min ((r2 - (upper_bound R)),s)) / 2 < s by A55, XXREAL_0:2;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) < (upper_bound R) + s by XREAL_1:8;

then A59: not (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in R2 by A50;

upper_bound R < (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) by A52, XREAL_1:29, XREAL_1:215;

then (upper_bound R) + ((min ((r2 - (upper_bound R)),s)) / 2) in R by A59, A58, A56, A57;

hence contradiction by A11, A53, SEQ_4:def 1; :: thesis: verum

( r in R2 & r < (upper_bound R) + s ) ; :: thesis: verum

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

then
lim S00 in F2
by A6, A7, A37, A41, Th1, Th3;
let n4 be Nat; :: thesis: S00 . n4 in F2

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: verum

end;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: verum

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: verum