let e, f be Real; :: 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 sequence of (bool REAL) st ( for i being Nat holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being Real st
( r in [.e,f.] & not r in A \/ B & ( for i being Nat ex k being 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 sequence of (bool REAL) st ( for i being Nat holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being Real st
( r in [.e,f.] & not r in A \/ B & ( for i being Nat ex k being 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 sequence of (bool REAL) st ( for i being Nat holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being Real st
( r in [.e,f.] & not r in A \/ B & ( for i being Nat ex k being Nat st
( i <= k & r in S . k ) ) )
let S be sequence of (bool REAL); :: thesis: ( ( for i being Nat holds
( S . i is interval & S . i meets A & S . i meets B ) ) implies ex r being Real st
( r in [.e,f.] & not r in A \/ B & ( for i being Nat ex k being Nat st
( i <= k & r in S . k ) ) ) )
assume A4: for i being Nat holds
( S . i is interval & S . i meets A & S . i meets B ) ; :: thesis: ex r being Real st
( r in [.e,f.] & not r in A \/ B & ( for i being Nat ex k being Nat st
( i <= k & r in S . k ) ) )
defpred S1[ set , Subset of REAL] means ( not $2 is empty & $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 object 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 object 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 ( not [.x,y.] is empty & [.x,y.] is closed_interval ) by A11, MEASURE5:14; :: 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; :: 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 ( not [.y,x.] is empty & [.y,x.] is closed_interval ) by A12, MEASURE5:14; :: 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; :: thesis: verum
end;
end;
end;
consider T being sequence of (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 ;
deffunc H1( Nat) -> Element of bool REAL = (T . $1) /\ B;
deffunc H2( Nat) -> Element of bool REAL = (T . $1) /\ A;
consider SA being sequence of (bool REAL) such that
A15: for i being Element of NAT holds SA . i = H2(i) from FUNCT_2:sch 4();
 consider SB being sequence of (bool REAL) such that
A16: for i being Element of NAT holds SB . i = H1(i) from FUNCT_2:sch 4();
 defpred S2[ Nat, Real, Real] means ( $2 in SA . $1 & $3 in SB . $1 & dist ((SA . $1),(SB . $1)) = |.($2 - $3).| );
A17: for i being Element of NAT ex ai, bi being Element of REAL st S2[i,ai,bi]
proof
let i be Element of NAT ; :: thesis: ex ai, bi being Element of REAL st S2[i,ai,bi]
reconsider Si = T . i as non empty 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, Th5;
consider ai, bi being Real such that
A21: ai in SAi and
A22: bi in SBi and
A23: dist (SAi,SBi) = |.(ai - bi).| by Th9;
reconsider ai = ai, bi = bi as Element of REAL by XREAL_0:def 1;
take ai ; :: thesis: ex bi being Element of 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 object ; :: 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 object such that
A25: x in dom sa and
A26: u = sa . x by FUNCT_1:def 3;
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 object ; :: 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 object such that
A31: x in dom (sb * Nseq) and
A32: u = (sb * Nseq) . x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A31;
(sb * Nseq) . n = sb . (Nseq . n) by FUNCT_2:15;
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:16;
then A38: (ga * Nseq1) + fb is convergent by A34, SEQ_2:5;
then A39: (1 / 2) (#) ((ga * Nseq1) + fb) is convergent by SEQ_2:7;
T . 0 meets A by A13;
then not A is empty ;
then dist (A,B) > 0 by A1, A14, Th11;
then A40: (dist (A,B)) / 2 > 0 by XREAL_1:139;
((lim (ga * Nseq1)) + (lim fb)) / 2 = (1 / 2) * ((lim (ga * Nseq1)) + (lim fb))
.= (1 / 2) * (lim ((ga * Nseq1) + fb)) by A34, A37, SEQ_2:6
.= lim ((1 / 2) (#) ((ga * Nseq1) + fb)) by A38, SEQ_2:8 ;
then consider k0 being Nat such that
A41: for i being Nat st k0 <= i holds
|.((((1 / 2) (#) ((ga * Nseq1) + fb)) . i) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < (dist (A,B)) / 2 by A39, A40, SEQ_2:def 7;
A42: k0 in NAT by ORDINAL1:def 12;
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 Nat ex k being Nat st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) ) )
lim (ga * Nseq1) = lim ga by A28, SEQ_4:17;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.e,f.] by A29, A35, Th1; :: thesis: ( not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B & ( for i being Nat ex k being Nat st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) ) )
now :: thesis: not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B
set i = Nseq . (Nseq1 . k0);
set di = dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))));
A43: 2 * |.((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| = |.2.| * |.((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| by ABSVALUE:def 1
.= |.(2 * ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))).| by COMPLEX1:65
.= |.(((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))).| ;
A44: (ga * Nseq1) . k0 = ga . (Nseq1 . k0) by FUNCT_2:15, A42
.= sa . (Nseq . (Nseq1 . k0)) by A30, FUNCT_2:15 ;
T . (Nseq . (Nseq1 . k0)) meets B by A13;
then (T . (Nseq . (Nseq1 . k0))) /\ B <> {} ;
then A45: not SB . (Nseq . (Nseq1 . k0)) is empty by A16;
A46: SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B by A16;
then A47: SB . (Nseq . (Nseq1 . k0)) c= B by XBOOLE_1:17;
A48: SB . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) by A46, XBOOLE_1:17;
A49: SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A by A15;
then A50: SA . (Nseq . (Nseq1 . k0)) c= A by XBOOLE_1:17;
T . (Nseq . (Nseq1 . k0)) meets A by A13;
then (T . (Nseq . (Nseq1 . k0))) /\ A <> {} ;
then A51: not SA . (Nseq . (Nseq1 . k0)) is empty by A15;
then A52: dist (A,B) <= dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A45, A50, A47, Th8;
(dist (A,B)) / 2 <= (dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2 by A51, A45, A50, A47, Th8, XREAL_1:72;
then A53: ((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:6;
((1 / 2) (#) ((ga * Nseq1) + fb)) . k0 = (1 / 2) * (((ga * Nseq1) + fb) . k0) by SEQ_1:9
.= (((ga * Nseq1) + fb) . k0) / 2
.= (((ga * Nseq1) . k0) + (fb . k0)) / 2 by SEQ_1:7 ;
then A54: |.(((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < (dist (A,B)) / 2 by A41;
( not T . (Nseq . (Nseq1 . k0)) is empty & T . (Nseq . (Nseq1 . k0)) is closed_interval ) by A13;
then A55: ex a, b being Real st
( a <= b & T . (Nseq . (Nseq1 . k0)) = [.a,b.] ) by MEASURE5:14;
A56: sb . (Nseq . (Nseq1 . k0)) in SB . (Nseq . (Nseq1 . k0)) by A24;
A57: SA . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) by A49, XBOOLE_1:17;
A58: fb . k0 = (sb * Nseq) . (Nseq1 . k0) by A36, FUNCT_2:15, A42
.= sb . (Nseq . (Nseq1 . k0)) by FUNCT_2:15 ;
2 * ((dist (A,B)) / 2) = dist (A,B) ;
then A59: 2 * |.((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < dist (A,B) by A54, A44, A58, XREAL_1:68;
A60: sa . (Nseq . (Nseq1 . k0)) in SA . (Nseq . (Nseq1 . k0)) by A24;
then A61: dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) <= |.((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))).| by A56, Th7;
A62: now :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0))
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:48;
then dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A61, ABSVALUE:def 1;
then dist (A,B) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A52, XXREAL_0:2;
then |.(((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))).| <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A59, A43, XXREAL_0:2;
then A63: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sa . (Nseq . (Nseq1 . k0))),(sb . (Nseq . (Nseq1 . k0))).] by RCOMP_1:2;
[.(sa . (Nseq . (Nseq1 . k0))),(sb . (Nseq . (Nseq1 . k0))).] c= T . (Nseq . (Nseq1 . k0)) by A55, A60, A56, A57, A48, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A63; :: thesis: verum
end;
suppose A64: sb . (Nseq . (Nseq1 . k0)) <= sa . (Nseq . (Nseq1 . k0)) ; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0))
A65: |.((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))).| = |.((sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0)))).| by UNIFORM1:11;
(sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) >= 0 by A64, XREAL_1:48;
then dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A61, A65, ABSVALUE:def 1;
then dist (A,B) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A52, XXREAL_0:2;
then |.(((sb . (Nseq . (Nseq1 . k0))) + (sa . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))).| <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A59, A43, XXREAL_0:2;
then A66: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sb . (Nseq . (Nseq1 . k0))),(sa . (Nseq . (Nseq1 . k0))).] by RCOMP_1:2;
[.(sb . (Nseq . (Nseq1 . k0))),(sa . (Nseq . (Nseq1 . k0))).] c= T . (Nseq . (Nseq1 . k0)) by A55, A60, A56, A57, A48, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A66; :: thesis: verum
end;
end;
end;
assume A67: ((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 A67, XBOOLE_0:def 3;
suppose A68: ((lim (ga * Nseq1)) + (lim fb)) / 2 in B ; :: thesis: contradiction
SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B by A16;
then A69: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SB . (Nseq . (Nseq1 . k0)) by A62, A68, XBOOLE_0:def 4;
A70: |.((((ga * Nseq1) . k0) - (fb . k0)) / 2).| = |.(((ga * Nseq1) . k0) - (fb . k0)).| / |.2.| by COMPLEX1:67
.= |.(((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 A71: |.(((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)).| by COMPLEX1:56;
|.((((ga * Nseq1) . k0) - (fb . k0)) / 2).| + |.(((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < |.((((ga * Nseq1) . k0) - (fb . k0)) / 2).| + ((dist (A,B)) / 2) by A54, XREAL_1:6;
then |.(((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < (|.(((ga * Nseq1) . k0) - (fb . k0)).| / 2) + ((dist (A,B)) / 2) by A71, A70, XXREAL_0:2;
then |.(((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, A44, A58;
then A72: |.(((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A53, XXREAL_0:2;
(ga * Nseq1) . k0 in SA . (Nseq . (Nseq1 . k0)) by A24, A44;
hence contradiction by A69, A72, Th7; :: thesis: verum
end;
suppose A73: ((lim (ga * Nseq1)) + (lim fb)) / 2 in A ; :: thesis: contradiction
SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A by A15;
then A74: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SA . (Nseq . (Nseq1 . k0)) by A62, A73, XBOOLE_0:def 4;
A75: |.(((fb . k0) - ((ga * Nseq1) . k0)) / 2).| = |.((fb . k0) - ((ga * Nseq1) . k0)).| / |.2.| by COMPLEX1:67
.= |.((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 A76: |.((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)).| by COMPLEX1:56;
A77: |.((fb . k0) - ((ga * Nseq1) . k0)).| = |.(((ga * Nseq1) . k0) - (fb . k0)).| by UNIFORM1:11
.= dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A24, A44, A58 ;
|.(((fb . k0) - ((ga * Nseq1) . k0)) / 2).| + |.((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < |.(((fb . k0) - ((ga * Nseq1) . k0)) / 2).| + ((dist (A,B)) / 2) by A54, XREAL_1:6;
then |.((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < (|.((fb . k0) - ((ga * Nseq1) . k0)).| / 2) + ((dist (A,B)) / 2) by A76, A75, XXREAL_0:2;
then A78: |.((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A53, A77, XXREAL_0:2;
fb . k0 in SB . (Nseq . (Nseq1 . k0)) by A24, A58;
hence contradiction by A74, A78, Th7; :: thesis: verum
end;
end;
end;
hence not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B ; :: thesis: for i being Nat ex k being Nat st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k )
let i be Nat; :: thesis: ex k being Nat st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k )
set k = max (k0,i);
A79: max (k0,i) in NAT by ORDINAL1:def 12;
take j = Nseq . (Nseq1 . (max (k0,i))); :: thesis: ( i <= j & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j )
A80: fb . (max (k0,i)) = (sb * Nseq) . (Nseq1 . (max (k0,i))) by A36, FUNCT_2:15, A79
.= sb . j by FUNCT_2:15 ;
A81: i <= max (k0,i) by XXREAL_0:25;
A82: sb . j in SB . j by A24;
T . j meets B by A13;
then (T . j) /\ B <> {} ;
then A83: not SB . j is empty by A16;
A84: dom Nseq = NAT by FUNCT_2:def 1;
T . j meets A by A13;
then (T . j) /\ A <> {} ;
then A85: not SA . j is empty by A15;
A86: i <= Nseq . i by SEQM_3:14;
A87: SA . j = (T . j) /\ A by A15;
then A88: 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 A79, SEQ_1:9
.= (((ga * Nseq1) + fb) . (max (k0,i))) / 2
.= (((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i)))) / 2 by A79, SEQ_1:7 ;
then A89: |.(((((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < (dist (A,B)) / 2 by A41, A79, XXREAL_0:25;
A90: 2 * ((dist (A,B)) / 2) = dist (A,B) ;
(ga * Nseq1) . (max (k0,i)) = ga . (Nseq1 . (max (k0,i))) by FUNCT_2:15, A79
.= sa . j by A30, FUNCT_2:15 ;
then A91: 2 * |.((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| < dist (A,B) by A89, A80, A90, XREAL_1:68;
( not T . j is empty & T . j is closed_interval ) by A13;
then A92: ex a, b being Real st
( a <= b & T . j = [.a,b.] ) by MEASURE5:14;
A93: SB . j = (T . j) /\ B by A16;
then A94: SB . j c= B by XBOOLE_1:17;
A95: SB . j c= T . j by A93, XBOOLE_1:17;
A96: i in NAT by ORDINAL1:def 12;
dom Nseq1 = NAT by FUNCT_2:def 1;
then Nseq1 . i <= Nseq1 . (max (k0,i)) by A81, VALUED_0:def 15, A79, A96;
then A97: Nseq . (Nseq1 . i) <= j by A84, VALUED_0:def 15;
i <= Nseq1 . i by SEQM_3:14;
then Nseq . i <= Nseq . (Nseq1 . i) by A84, VALUED_0:def 15, A96;
then i <= Nseq . (Nseq1 . i) by A86, XXREAL_0:2;
hence i <= j by A97, XXREAL_0:2; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j
set di = dist ((SA . j),(SB . j));
A98: 2 * |.((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| = |.2.| * |.((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)).| by ABSVALUE:def 1
.= |.(2 * ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))).| by COMPLEX1:65
.= |.(((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))).| ;
SA . j c= A by A87, XBOOLE_1:17;
then A99: dist (A,B) <= dist ((SA . j),(SB . j)) by A85, A83, A94, Th8;
A100: sa . j in SA . j by A24;
then A101: dist ((SA . j),(SB . j)) <= |.((sb . j) - (sa . j)).| by A82, Th7;
A102: now :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j
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:48;
then dist ((SA . j),(SB . j)) <= (sb . j) - (sa . j) by A101, ABSVALUE:def 1;
then dist (A,B) <= (sb . j) - (sa . j) by A99, XXREAL_0:2;
then |.(((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))).| <= (sb . j) - (sa . j) by A91, A98, XXREAL_0:2;
then A103: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sa . j),(sb . j).] by RCOMP_1:2;
[.(sa . j),(sb . j).] c= T . j by A92, A100, A82, A88, A95, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A103; :: thesis: verum
end;
suppose A104: sb . j <= sa . j ; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j
A105: |.((sb . j) - (sa . j)).| = |.((sa . j) - (sb . j)).| by UNIFORM1:11;
(sa . j) - (sb . j) >= 0 by A104, XREAL_1:48;
then dist ((SA . j),(SB . j)) <= (sa . j) - (sb . j) by A101, A105, ABSVALUE:def 1;
then dist (A,B) <= (sa . j) - (sb . j) by A99, XXREAL_0:2;
then |.(((sb . j) + (sa . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))).| <= (sa . j) - (sb . j) by A91, A98, XXREAL_0:2;
then A106: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sb . j),(sa . j).] by RCOMP_1:2;
[.(sb . j),(sa . j).] c= T . j by A92, A100, A82, A88, A95, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A106; :: thesis: verum
end;
end;
end;
T . j c= S . j by A13;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j by A102; :: thesis: verum