let e, f be real number ; :: thesis: for A, B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] holds
for S being Function of NAT ,(bool REAL ) st ( for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) )
let A, B be compact Subset of REAL ; :: thesis: ( A misses B & A c= [.e,f.] & B c= [.e,f.] implies for S being Function of NAT ,(bool REAL ) st ( for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) ) )
assume that
A1: A misses B and
A2: A c= [.e,f.] and
A3: B c= [.e,f.] ; :: thesis: for S being Function of NAT ,(bool REAL ) st ( for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) )
let S be Function of NAT ,(bool REAL ); :: thesis: ( ( for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ) implies ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) ) )
assume A4: for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ; :: thesis: ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) )
defpred S1[ set , Subset of REAL ] means ( $2 is closed-interval & $2 meets A & $2 meets B & $2 c= S . $1 );
A5: for i being Element of NAT ex u being Subset of REAL st S1[i,u]
proof
let i be Element of NAT ; :: thesis: ex u being Subset of REAL st S1[i,u]
A6: S . i is interval by A4;
S . i meets B by A4;
then consider y being set such that
A7: y in S . i and
A8: y in B by XBOOLE_0:3;
S . i meets A by A4;
then consider x being set such that
A9: x in S . i and
A10: x in A by XBOOLE_0:3;
reconsider y = y as Real by A8;
reconsider x = x as Real by A10;
per cases ( x <= y or y <= x ) ;
suppose A11: x <= y ; :: thesis: ex u being Subset of REAL st S1[i,u]
take [.x,y.] ; :: thesis: S1[i,[.x,y.]]
thus [.x,y.] is closed-interval by A11, INTEGRA1:def 1; :: thesis: ( [.x,y.] meets A & [.x,y.] meets B & [.x,y.] c= S . i )
x in [.x,y.] by A11;
hence [.x,y.] meets A by A10, XBOOLE_0:3; :: thesis: ( [.x,y.] meets B & [.x,y.] c= S . i )
y in [.x,y.] by A11;
hence [.x,y.] meets B by A8, XBOOLE_0:3; :: thesis: [.x,y.] c= S . i
thus [.x,y.] c= S . i by A9, A7, A6, XXREAL_2:def 12; :: thesis: verum
end;
suppose A12: y <= x ; :: thesis: ex u being Subset of REAL st S1[i,u]
take [.y,x.] ; :: thesis: S1[i,[.y,x.]]
thus [.y,x.] is closed-interval by A12, INTEGRA1:def 1; :: thesis: ( [.y,x.] meets A & [.y,x.] meets B & [.y,x.] c= S . i )
x in [.y,x.] by A12;
hence [.y,x.] meets A by A10, XBOOLE_0:3; :: thesis: ( [.y,x.] meets B & [.y,x.] c= S . i )
y in [.y,x.] by A12;
hence [.y,x.] meets B by A8, XBOOLE_0:3; :: thesis: [.y,x.] c= S . i
thus [.y,x.] c= S . i by A9, A7, A6, XXREAL_2:def 12; :: thesis: verum
end;
end;
end;
consider T being Function of NAT ,(bool REAL ) such that
A13: for i being Element of NAT holds S1[i,T . i] from FUNCT_2:sch 3(A5);
 T . 0 meets B by A13;
then A14: not B is empty by XBOOLE_1:65;
deffunc H1( Element of NAT ) -> Element of bool REAL = (T . $1) /\ B;
deffunc H2( Element of NAT ) -> Element of bool REAL = (T . $1) /\ A;
consider SA being Function of NAT ,(bool REAL ) such that
A15: for i being Element of NAT holds SA . i = H2(i) from FUNCT_2:sch 4();
 consider SB being Function of NAT ,(bool REAL ) such that
A16: for i being Element of NAT holds SB . i = H1(i) from FUNCT_2:sch 4();
 defpred S2[ Element of NAT , Real, Real] means ( $2 in SA . $1 & $3 in SB . $1 & dist (SA . $1),(SB . $1) = abs ($2 - $3) );
A17: for i being Element of NAT ex ai, bi being Real st S2[i,ai,bi]
proof
let i be Element of NAT ; :: thesis: ex ai, bi being Real st S2[i,ai,bi]
reconsider Si = T . i as closed-interval Subset of REAL by A13;
A18: T . i meets B by A13;
A19: SA . i = Si /\ A by A15;
A20: SB . i = Si /\ B by A16;
T . i meets A by A13;
then reconsider SAi = SA . i, SBi = SB . i as non empty compact Subset of REAL by A18, A19, A20, Th14, XBOOLE_0:def 7;
consider ai, bi being real number such that
A21: ai in SAi and
A22: bi in SBi and
A23: dist SAi,SBi = abs (ai - bi) by Th18;
reconsider ai = ai, bi = bi as Real by XREAL_0:def 1;
take ai ; :: thesis: ex bi being Real st S2[i,ai,bi]
take bi ; :: thesis: S2[i,ai,bi]
thus S2[i,ai,bi] by A21, A22, A23; :: thesis: verum
end;
consider sa, sb being Real_Sequence such that
A24: for i being Element of NAT holds S2[i,sa . i,sb . i] from JCT_MISC:sch 2(A17);
 rng sa c= [.e,f.]
proof
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng sa or u in [.e,f.] )
assume u in rng sa ; :: thesis: u in [.e,f.]
then consider x being set such that
A25: x in dom sa and
A26: u = sa . x by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A25;
sa . n in SA . n by A24;
then u in (T . n) /\ A by A15, A26;
then u in A by XBOOLE_0:def 4;
hence u in [.e,f.] by A2; :: thesis: verum
end;
then consider ga being Real_Sequence such that
A27: ga is subsequence of sa and
A28: ga is convergent and
A29: lim ga in [.e,f.] by RCOMP_1:def 3;
consider Nseq being increasing sequence of NAT such that
A30: ga = sa * Nseq by A27, VALUED_0:def 17;
set gb = sb * Nseq;
rng (sb * Nseq) c= [.e,f.]
proof
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng (sb * Nseq) or u in [.e,f.] )
assume u in rng (sb * Nseq) ; :: thesis: u in [.e,f.]
then consider x being set such that
A31: x in dom (sb * Nseq) and
A32: u = (sb * Nseq) . x by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A31;
(sb * Nseq) . n = sb . (Nseq . n) by FUNCT_2:21;
then (sb * Nseq) . n in SB . (Nseq . n) by A24;
then u in (T . (Nseq . n)) /\ B by A16, A32;
then u in B by XBOOLE_0:def 4;
hence u in [.e,f.] by A3; :: thesis: verum
end;
then consider fb being Real_Sequence such that
A33: fb is subsequence of sb * Nseq and
A34: fb is convergent and
A35: lim fb in [.e,f.] by RCOMP_1:def 3;
consider Nseq1 being increasing sequence of NAT such that
A36: fb = (sb * Nseq) * Nseq1 by A33, VALUED_0:def 17;
set fa = ga * Nseq1;
set r = ((lim (ga * Nseq1)) + (lim fb)) / 2;
set d0 = dist A,B;
set ff = (1 / 2) (#) ((ga * Nseq1) + fb);
A37: ga * Nseq1 is convergent by A28, SEQ_4:29;
then A38: (ga * Nseq1) + fb is convergent by A34, SEQ_2:19;
then A39: (1 / 2) (#) ((ga * Nseq1) + fb) is convergent by SEQ_2:21;
T . 0 meets A by A13;
then not A is empty by XBOOLE_1:65;
then dist A,B > 0 by A1, A14, Th20;
then A40: (dist A,B) / 2 > 0 by XREAL_1:141;
((lim (ga * Nseq1)) + (lim fb)) / 2 = (1 / 2) * ((lim (ga * Nseq1)) + (lim fb))
.= (1 / 2) * (lim ((ga * Nseq1) + fb)) by A34, A37, SEQ_2:20
.= lim ((1 / 2) (#) ((ga * Nseq1) + fb)) by A38, SEQ_2:22 ;
then consider k0 being Element of NAT such that
A41: for i being Element of NAT st k0 <= i holds
abs ((((1 / 2) (#) ((ga * Nseq1) + fb)) . i) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist A,B) / 2 by A39, A40, SEQ_2:def 7;
take ((lim (ga * Nseq1)) + (lim fb)) / 2 ; :: thesis: ( ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.e,f.] & not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) ) )
lim (ga * Nseq1) = lim ga by A28, SEQ_4:30;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.e,f.] by A29, A35, Th9; :: thesis: ( not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) ) )
now
set i = Nseq . (Nseq1 . k0);
set di = dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)));
A42: 2 * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) = (abs 2) * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by ABSVALUE:def 1
.= abs (2 * ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:151
.= abs (((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) ;
A43: (ga * Nseq1) . k0 = ga . (Nseq1 . k0) by FUNCT_2:21
.= sa . (Nseq . (Nseq1 . k0)) by A30, FUNCT_2:21 ;
T . (Nseq . (Nseq1 . k0)) meets B by A13;
then (T . (Nseq . (Nseq1 . k0))) /\ B <> {} by XBOOLE_0:def 7;
then A44: not SB . (Nseq . (Nseq1 . k0)) is empty by A16;
A45: SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B by A16;
then A46: SB . (Nseq . (Nseq1 . k0)) c= B by XBOOLE_1:17;
A47: SB . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) by A45, XBOOLE_1:17;
A48: SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A by A15;
then A49: SA . (Nseq . (Nseq1 . k0)) c= A by XBOOLE_1:17;
T . (Nseq . (Nseq1 . k0)) meets A by A13;
then (T . (Nseq . (Nseq1 . k0))) /\ A <> {} by XBOOLE_0:def 7;
then A50: not SA . (Nseq . (Nseq1 . k0)) is empty by A15;
then A51: dist A,B <= dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) by A44, A49, A46, Th17;
(dist A,B) / 2 <= (dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) / 2 by A50, A44, A49, A46, Th17, XREAL_1:74;
then A52: ((dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) / 2) + ((dist A,B) / 2) <= ((dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) / 2) + ((dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) / 2) by XREAL_1:8;
((1 / 2) (#) ((ga * Nseq1) + fb)) . k0 = (1 / 2) * (((ga * Nseq1) + fb) . k0) by SEQ_1:13
.= (((ga * Nseq1) + fb) . k0) / 2
.= (((ga * Nseq1) . k0) + (fb . k0)) / 2 by SEQ_1:11 ;
then A53: abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist A,B) / 2 by A41;
T . (Nseq . (Nseq1 . k0)) is closed-interval by A13;
then A54: ex a, b being Real st
( a <= b & T . (Nseq . (Nseq1 . k0)) = [.a,b.] ) by INTEGRA1:def 1;
A55: sb . (Nseq . (Nseq1 . k0)) in SB . (Nseq . (Nseq1 . k0)) by A24;
A56: SA . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) by A48, XBOOLE_1:17;
A57: fb . k0 = (sb * Nseq) . (Nseq1 . k0) by A36, FUNCT_2:21
.= sb . (Nseq . (Nseq1 . k0)) by FUNCT_2:21 ;
2 * ((dist A,B) / 2) = dist A,B ;
then A58: 2 * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < dist A,B by A53, A43, A57, XREAL_1:70;
A59: sa . (Nseq . (Nseq1 . k0)) in SA . (Nseq . (Nseq1 . k0)) by A24;
then A60: dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) <= abs ((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))) by A55, Th16;
A61: now
per cases ( sa . (Nseq . (Nseq1 . k0)) <= sb . (Nseq . (Nseq1 . k0)) or sb . (Nseq . (Nseq1 . k0)) <= sa . (Nseq . (Nseq1 . k0)) ) ;
suppose sa . (Nseq . (Nseq1 . k0)) <= sb . (Nseq . (Nseq1 . k0)) ; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0))
then (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) >= 0 by XREAL_1:50;
then dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A60, ABSVALUE:def 1;
then dist A,B <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A51, XXREAL_0:2;
then abs (((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A58, A42, XXREAL_0:2;
then A62: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sa . (Nseq . (Nseq1 . k0))),(sb . (Nseq . (Nseq1 . k0))).] by RCOMP_1:9;
[.(sa . (Nseq . (Nseq1 . k0))),(sb . (Nseq . (Nseq1 . k0))).] c= T . (Nseq . (Nseq1 . k0)) by A54, A59, A55, A56, A47, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A62; :: thesis: verum
end;
suppose A63: sb . (Nseq . (Nseq1 . k0)) <= sa . (Nseq . (Nseq1 . k0)) ; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0))
A64: abs ((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))) = abs ((sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0)))) by UNIFORM1:13;
(sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) >= 0 by A63, XREAL_1:50;
then dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A60, A64, ABSVALUE:def 1;
then dist A,B <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A51, XXREAL_0:2;
then abs (((sb . (Nseq . (Nseq1 . k0))) + (sa . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A58, A42, XXREAL_0:2;
then A65: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sb . (Nseq . (Nseq1 . k0))),(sa . (Nseq . (Nseq1 . k0))).] by RCOMP_1:9;
[.(sb . (Nseq . (Nseq1 . k0))),(sa . (Nseq . (Nseq1 . k0))).] c= T . (Nseq . (Nseq1 . k0)) by A54, A59, A55, A56, A47, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A65; :: thesis: verum
end;
end;
end;
assume A66: ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B ; :: thesis: contradiction
per cases ( ((lim (ga * Nseq1)) + (lim fb)) / 2 in B or ((lim (ga * Nseq1)) + (lim fb)) / 2 in A ) by A66, XBOOLE_0:def 3;
suppose A67: ((lim (ga * Nseq1)) + (lim fb)) / 2 in B ; :: thesis: contradiction
SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B by A16;
then A68: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SB . (Nseq . (Nseq1 . k0)) by A61, A67, XBOOLE_0:def 4;
A69: abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2) = (abs (((ga * Nseq1) . k0) - (fb . k0))) / (abs 2) by COMPLEX1:153
.= (abs (((ga * Nseq1) . k0) - (fb . k0))) / 2 by ABSVALUE:def 1 ;
((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2) = ((((ga * Nseq1) . k0) - (fb . k0)) / 2) + (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) ;
then A70: abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) <= (abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + (abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:142;
(abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + (abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < (abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + ((dist A,B) / 2) by A53, XREAL_1:8;
then abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((abs (((ga * Nseq1) . k0) - (fb . k0))) / 2) + ((dist A,B) / 2) by A70, A69, XXREAL_0:2;
then abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) / 2) + ((dist A,B) / 2) by A24, A43, A57;
then A71: abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) by A52, XXREAL_0:2;
(ga * Nseq1) . k0 in SA . (Nseq . (Nseq1 . k0)) by A24, A43;
hence contradiction by A68, A71, Th16; :: thesis: verum
end;
suppose A72: ((lim (ga * Nseq1)) + (lim fb)) / 2 in A ; :: thesis: contradiction
SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A by A15;
then A73: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SA . (Nseq . (Nseq1 . k0)) by A61, A72, XBOOLE_0:def 4;
A74: abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2) = (abs ((fb . k0) - ((ga * Nseq1) . k0))) / (abs 2) by COMPLEX1:153
.= (abs ((fb . k0) - ((ga * Nseq1) . k0))) / 2 by ABSVALUE:def 1 ;
(fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2) = (((fb . k0) - ((ga * Nseq1) . k0)) / 2) + ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) ;
then A75: abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) <= (abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + (abs ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:142;
A76: abs ((fb . k0) - ((ga * Nseq1) . k0)) = abs (((ga * Nseq1) . k0) - (fb . k0)) by UNIFORM1:13
.= dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) by A24, A43, A57 ;
(abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + (abs ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < (abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + ((dist A,B) / 2) by A53, XREAL_1:8;
then abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((abs ((fb . k0) - ((ga * Nseq1) . k0))) / 2) + ((dist A,B) / 2) by A75, A74, XXREAL_0:2;
then A77: abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) by A52, A76, XXREAL_0:2;
fb . k0 in SB . (Nseq . (Nseq1 . k0)) by A24, A57;
hence contradiction by A73, A77, Th16; :: thesis: verum
end;
end;
end;
hence not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B ; :: thesis: for i being Element of NAT ex k being Element of NAT st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k )
let i be Element of NAT ; :: thesis: ex k being Element of NAT st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k )
set k = max k0,i;
take j = Nseq . (Nseq1 . (max k0,i)); :: thesis: ( i <= j & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j )
A78: fb . (max k0,i) = (sb * Nseq) . (Nseq1 . (max k0,i)) by A36, FUNCT_2:21
.= sb . j by FUNCT_2:21 ;
A79: i <= max k0,i by XXREAL_0:25;
A80: sb . j in SB . j by A24;
T . j meets B by A13;
then (T . j) /\ B <> {} by XBOOLE_0:def 7;
then A81: not SB . j is empty by A16;
A82: dom Nseq = NAT by FUNCT_2:def 1;
T . j meets A by A13;
then (T . j) /\ A <> {} by XBOOLE_0:def 7;
then A83: not SA . j is empty by A15;
A84: i <= Nseq . i by SEQM_3:33;
A85: SA . j = (T . j) /\ A by A15;
then A86: SA . j c= T . j by XBOOLE_1:17;
((1 / 2) (#) ((ga * Nseq1) + fb)) . (max k0,i) = (1 / 2) * (((ga * Nseq1) + fb) . (max k0,i)) by SEQ_1:13
.= (((ga * Nseq1) + fb) . (max k0,i)) / 2
.= (((ga * Nseq1) . (max k0,i)) + (fb . (max k0,i))) / 2 by SEQ_1:11 ;
then A87: abs (((((ga * Nseq1) . (max k0,i)) + (fb . (max k0,i))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist A,B) / 2 by A41, XXREAL_0:25;
A88: 2 * ((dist A,B) / 2) = dist A,B ;
(ga * Nseq1) . (max k0,i) = ga . (Nseq1 . (max k0,i)) by FUNCT_2:21
.= sa . j by A30, FUNCT_2:21 ;
then A89: 2 * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < dist A,B by A87, A78, A88, XREAL_1:70;
T . j is closed-interval by A13;
then A90: ex a, b being Real st
( a <= b & T . j = [.a,b.] ) by INTEGRA1:def 1;
A91: SB . j = (T . j) /\ B by A16;
then A92: SB . j c= B by XBOOLE_1:17;
A93: SB . j c= T . j by A91, XBOOLE_1:17;
dom Nseq1 = NAT by FUNCT_2:def 1;
then Nseq1 . i <= Nseq1 . (max k0,i) by A79, VALUED_0:def 15;
then A94: Nseq . (Nseq1 . i) <= j by A82, VALUED_0:def 15;
i <= Nseq1 . i by SEQM_3:33;
then Nseq . i <= Nseq . (Nseq1 . i) by A82, VALUED_0:def 15;
then i <= Nseq . (Nseq1 . i) by A84, XXREAL_0:2;
hence i <= j by A94, XXREAL_0:2; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j
set di = dist (SA . j),(SB . j);
A95: 2 * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) = (abs 2) * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by ABSVALUE:def 1
.= abs (2 * ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:151
.= abs (((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) ;
SA . j c= A by A85, XBOOLE_1:17;
then A96: dist A,B <= dist (SA . j),(SB . j) by A83, A81, A92, Th17;
A97: sa . j in SA . j by A24;
then A98: dist (SA . j),(SB . j) <= abs ((sb . j) - (sa . j)) by A80, Th16;
A99: now
per cases ( sa . j <= sb . j or sb . j <= sa . j ) ;
suppose sa . j <= sb . j ; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j
then (sb . j) - (sa . j) >= 0 by XREAL_1:50;
then dist (SA . j),(SB . j) <= (sb . j) - (sa . j) by A98, ABSVALUE:def 1;
then dist A,B <= (sb . j) - (sa . j) by A96, XXREAL_0:2;
then abs (((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sb . j) - (sa . j) by A89, A95, XXREAL_0:2;
then A100: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sa . j),(sb . j).] by RCOMP_1:9;
[.(sa . j),(sb . j).] c= T . j by A90, A97, A80, A86, A93, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A100; :: thesis: verum
end;
suppose A101: sb . j <= sa . j ; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j
A102: abs ((sb . j) - (sa . j)) = abs ((sa . j) - (sb . j)) by UNIFORM1:13;
(sa . j) - (sb . j) >= 0 by A101, XREAL_1:50;
then dist (SA . j),(SB . j) <= (sa . j) - (sb . j) by A98, A102, ABSVALUE:def 1;
then dist A,B <= (sa . j) - (sb . j) by A96, XXREAL_0:2;
then abs (((sb . j) + (sa . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sa . j) - (sb . j) by A89, A95, XXREAL_0:2;
then A103: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sb . j),(sa . j).] by RCOMP_1:9;
[.(sb . j),(sa . j).] c= T . j by A90, A97, A80, A86, A93, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A103; :: thesis: verum
end;
end;
end;
T . j c= S . j by A13;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j by A99; :: thesis: verum