let X be non empty MetrSpace; :: thesis: for f being Function of I[01],()
for F1, F2 being Subset of ()
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],(); :: thesis: for F1, F2 being Subset of ()
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 (); :: 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
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:
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;
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: ( 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;
r2 is UpperBound of R
proof
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;
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: ( 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 ;
hence x in [.0,1.] by ; :: thesis: verum
end;
then reconsider S1 = s1 as sequence of () by ;
A17: I[01] = TopSpaceMetr () by ;
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 () by ;
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 ;
then S2 is convergent by Th7;
then lim S2 = lim S1 by Th7;
then A20: lim s1 = lim S1 by ;
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: ( 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 ()
for w1 being Point of X st w1 = f . w & dist ((lim S1),w) < r7 holds
dist (t1,w1) < r by ;
consider n0 being Nat such that
A24: for m being Nat st m >= n0 holds
dist ((S1 . m),(lim S1)) < r7 by ;
for m being Nat st m >= n0 holds
dist ((S00 . m),t1) < r
proof
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 ;
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 ; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r ; :: thesis: verum
end;
A27: r2 >= upper_bound R by ;
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: ( 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:
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;
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: ( r in R2 implies r >= upper_bound R )
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: verum
end;
upper_bound R is LowerBound of R2
proof
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:
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;
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 ;
{ 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: ( 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 ;
hence x in [.0,1.] by ; :: thesis: verum
end;
then reconsider S1 = s2 as sequence of () by ;
reconsider S2 = s2 as sequence of RealSpace by METRIC_1:def 13;
A37: S1 is convergent by ;
then S2 is convergent by Th7;
then lim S2 = lim S1 by Th7;
then A38: lim s2 = lim S1 by ;
for n4 being Nat holds S00 . n4 in F1
proof
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 ;
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 ; :: thesis: verum
end;
then lim S00 in F1 by A5, A7, A19, A17, Th1, Th3;
then A40: f . (lim s1) in F1 by ;
A41: I[01] = TopSpaceMetr () by ;
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 () by ;
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: ( 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 ()
for w1 being Point of X st w1 = f . w & dist ((lim S1),w) < r7 holds
dist (t1,w1) < r by ;
consider n0 being Nat such that
A45: for m being Nat st m >= n0 holds
dist ((S1 . m),(lim S1)) < r7 by ;
for m being Nat st m >= n0 holds
dist ((S00 . m),t1) < r
proof
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 ;
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 ; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st m >= n holds
dist ((S00 . m),t1) < r ; :: thesis: verum
end;
A48: r1 <= upper_bound R by ;
for s being Real st 0 < s holds
ex r being Real st
( r in R2 & r < () + s )
proof
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in R2 & r < () + s ) )

assume A49: 0 < s ; :: thesis: ex r being Real st
( r in R2 & r < () + s )

now :: thesis: ex r being Real st
( r < () + s & r in R2 )
assume A50: for r being Real st r < () + s holds
not r in R2 ; :: thesis: contradiction
now :: thesis: ( ( r2 - () = 0 & contradiction ) or ( r2 - () > 0 & contradiction ) )
per cases ( r2 - () = 0 or r2 - () > 0 ) by ;
case A51: r2 - () > 0 ; :: thesis: contradiction
set rs0 = min ((r2 - ()),s);
set r0 = () + ((min ((r2 - ()),s)) / 2);
A52: min ((r2 - ()),s) > 0 by ;
then A53: upper_bound R < () + ((min ((r2 - ()),s)) / 2) by ;
min ((r2 - ()),s) <= r2 - () by XXREAL_0:17;
then A54: (upper_bound R) + (min ((r2 - ()),s)) <= () + (r2 - ()) by XREAL_1:7;
A55: (min ((r2 - ()),s)) / 2 < min ((r2 - ()),s) by ;
then (upper_bound R) + ((min ((r2 - ()),s)) / 2) < () + (min ((r2 - ()),s)) by XREAL_1:8;
then A56: (upper_bound R) + ((min ((r2 - ()),s)) / 2) <= r2 by ;
then (upper_bound R) + ((min ((r2 - ()),s)) / 2) <= 1 by ;
then (upper_bound R) + ((min ((r2 - ()),s)) / 2) in the carrier of I[01] by ;
then (upper_bound R) + ((min ((r2 - ()),s)) / 2) in dom f by FUNCT_2:def 1;
then f . (() + ((min ((r2 - ()),s)) / 2)) in rng f by FUNCT_1:def 3;
then f . (() + ((min ((r2 - ()),s)) / 2)) in the carrier of () ;
then f . (() + ((min ((r2 - ()),s)) / 2)) in the carrier of X by TOPMETR:12;
then A57: ( f . (() + ((min ((r2 - ()),s)) / 2)) in F1 or f . (() + ((min ((r2 - ()),s)) / 2)) in F2 ) by ;
upper_bound R <= () + ((min ((r2 - ()),s)) / 2) by ;
then A58: r1 <= () + ((min ((r2 - ()),s)) / 2) by ;
min ((r2 - ()),s) <= s by XXREAL_0:17;
then (min ((r2 - ()),s)) / 2 < s by ;
then (upper_bound R) + ((min ((r2 - ()),s)) / 2) < () + s by XREAL_1:8;
then A59: not (upper_bound R) + ((min ((r2 - ()),s)) / 2) in R2 by A50;
upper_bound R < () + ((min ((r2 - ()),s)) / 2) by ;
then (upper_bound R) + ((min ((r2 - ()),s)) / 2) in R by A59, A58, A56, A57;
hence contradiction by A11, A53, SEQ_4:def 1; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence ex r being Real st
( r in R2 & r < () + s ) ; :: thesis: verum
end;
then A60: upper_bound R = lower_bound R2 by ;
S00 is convergent by A7, A31, A41, Th3, Th8;
then A61: f . (lim S1) = lim S00 by ;
for n4 being Nat holds S00 . n4 in F2
proof
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 ;
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 ; :: thesis: verum
end;
then lim S00 in F2 by A6, A7, A37, A41, Th1, Th3;
then f . (lim s1) in F1 /\ F2 by ;
hence ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 ) by ; :: thesis: verum