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 connected & 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 connected & 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 connected & 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 connected & 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 connected & 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 S₁[ 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 S₁[i,u]

proof

let i be Element of NAT ; :: thesis: ex u being Subset of REAL st S₁[i,u]
S . i meets A by A4;
then consider x being set such that
A6: x in S . i and
A7: x in A by XBOOLE_0:3;
reconsider x = x as Real by A7;
S . i meets B by A4;
then consider y being set such that
A8: y in S . i and
A9: y in B by XBOOLE_0:3;
reconsider y = y as Real by A9;
A10: S . i is connected by A4;

per cases ( x <= y or y <= x ) ;

suppose A11: x <= y ; :: thesis: ex u being Subset of REAL st S₁[i,u]

take [.x,y.] ; :: thesis: S₁[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 A7, 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 A9, XBOOLE_0:3; :: thesis: [.x,y.] c= S . i
thus [.x,y.] c= S . i by A6, A8, A10, Def1; :: thesis: verum

end;

suppose A12: y <= x ; :: thesis: ex u being Subset of REAL st S₁[i,u]

take [.y,x.] ; :: thesis: S₁[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 A7, 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 A9, XBOOLE_0:3; :: thesis: [.y,x.] c= S . i
thus [.y,x.] c= S . i by A6, A8, A10, Def1; :: thesis: verum

end;

end;

end;

consider T being Function of NAT , bool REAL such that
A13: for i being Element of NAT holds S₁[i,T . i] from FUNCT_2:sch 3(A5);
deffunc H₁( Element of NAT ) -> Element of bool REAL = (T . $1) /\ A;
consider SA being Function of NAT , bool REAL such that
A14: for i being Element of NAT holds SA . i = H₁(i) from FUNCT_2:sch 4();
deffunc H₂( Element of NAT ) -> Element of bool REAL = (T . $1) /\ B;
consider SB being Function of NAT , bool REAL such that
A15: for i being Element of NAT holds SB . i = H₂(i) from FUNCT_2:sch 4();
defpred S₂[ Element of NAT , Real, Real] means ( $2 in SA . $1 & $3 in SB . $1 & dist (SA . $1),(SB . $1) = abs ($2 - $3) );
A16: for i being Element of NAT ex ai, bi being Real st S₂[i,ai,bi]

proof

let i be Element of NAT ; :: thesis: ex ai, bi being Real st S₂[i,ai,bi]
reconsider Si = T . i as closed-interval Subset of REAL by A13;
A17: ( T . i meets A & T . i meets B ) by A13;
( SA . i = Si /\ A & SB . i = Si /\ B ) by A14, A15;
then reconsider SAi = SA . i, SBi = SB . i as non empty compact Subset of REAL by A17, Th14, XBOOLE_0:def 7;
consider ai, bi being real number such that
A18: ( ai in SAi & bi in SBi & 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 S₂[i,ai,bi]
take bi ; :: thesis: S₂[i,ai,bi]
thus S₂[i,ai,bi] by A18; :: thesis: verum

end;

consider sa, sb being Real_Sequence such that
A19: for i being Element of NAT holds S₂[i,sa . i,sb . i] from JCT_MISC:sch 2(A16);
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
A20: x in dom sa and
A21: u = sa . x by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A20;
sa . n in SA . n by A19;
then u in (T . n) /\ A by A14, A21;
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
A22: ga is subsequence of sa and
A23: ga is convergent and
A24: lim ga in [.e,f.] by RCOMP_1:def 3;
consider Nseq being increasing sequence of NAT such that
A25: ga = sa * Nseq by A22, 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
A26: x in dom (sb * Nseq) and
A27: u = (sb * Nseq) . x by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A26;
(sb * Nseq) . n = sb . (Nseq . n) by FUNCT_2:21;
then (sb * Nseq) . n in SB . (Nseq . n) by A19;
then u in (T . (Nseq . n)) /\ B by A15, A27;
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
A28: fb is subsequence of sb * Nseq and
A29: fb is convergent and
A30: lim fb in [.e,f.] by RCOMP_1:def 3;
consider Nseq1 being increasing sequence of NAT such that
A31: fb = (sb * Nseq) * Nseq1 by A28, VALUED_0:def 17;
set fa = ga * Nseq1;
set r = ((lim (ga * Nseq1)) + (lim fb)) / 2;
A32: lim (ga * Nseq1) = lim ga by A23, SEQ_4:30;
set d0 = dist A,B;
set ff = (1 / 2) (#) ((ga * Nseq1) + fb);
A33: ga * Nseq1 is convergent by A23, SEQ_4:29;
then A34: (ga * Nseq1) + fb is convergent by A29, SEQ_2:19;
then A35: (1 / 2) (#) ((ga * Nseq1) + fb) is convergent by SEQ_2:21;
A36: ((lim (ga * Nseq1)) + (lim fb)) / 2 = (1 / 2) * ((lim (ga * Nseq1)) + (lim fb))
.= (1 / 2) * (lim ((ga * Nseq1) + fb)) by A29, A33, SEQ_2:20
.= lim ((1 / 2) (#) ((ga * Nseq1) + fb)) by A34, SEQ_2:22 ;
( T . 0 meets A & T . 0 meets B ) by A13;
then ( not A is empty & not B is empty ) by XBOOLE_1:65;
then dist A,B > 0 by A1, Th20;
then (dist A,B) / 2 > 0 by XREAL_1:141;
then consider k0 being Element of NAT such that
A37: 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 A35, A36, SEQ_2:def 7;

A38: now

assume A39: ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B ; :: thesis: contradiction
((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 A40: abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist A,B) / 2 by A37;
set i = Nseq . (Nseq1 . k0);
set di = dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)));
( T . (Nseq . (Nseq1 . k0)) meets A & T . (Nseq . (Nseq1 . k0)) meets B ) by A13;
then ( (T . (Nseq . (Nseq1 . k0))) /\ A <> {} & (T . (Nseq . (Nseq1 . k0))) /\ B <> {} ) by XBOOLE_0:def 7;
then A41: ( not SA . (Nseq . (Nseq1 . k0)) is empty & not SB . (Nseq . (Nseq1 . k0)) is empty ) by A14, A15;
A42: ( SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A & SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B ) by A14, A15;
then ( SA . (Nseq . (Nseq1 . k0)) c= A & SB . (Nseq . (Nseq1 . k0)) c= B ) by XBOOLE_1:17;
then A43: dist A,B <= dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) by A41, Th17;
then (dist A,B) / 2 <= (dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) / 2 by XREAL_1:74;
then A44: ((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;
A45: (ga * Nseq1) . k0 = ga . (Nseq1 . k0) by FUNCT_2:21
.= sa . (Nseq . (Nseq1 . k0)) by A25, FUNCT_2:21 ;
A46: fb . k0 = (sb * Nseq) . (Nseq1 . k0) by A31, FUNCT_2:21
.= sb . (Nseq . (Nseq1 . k0)) by FUNCT_2:21 ;
T . (Nseq . (Nseq1 . k0)) is closed-interval by A13;
then consider a, b being Real such that
a <= b and
A47: T . (Nseq . (Nseq1 . k0)) = [.a,b.] by INTEGRA1:def 1;
2 * ((dist A,B) / 2) = dist A,B ;
then A48: 2 * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < dist A,B by A40, A45, A46, XREAL_1:70;
A49: 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))) ;
A50: ( sa . (Nseq . (Nseq1 . k0)) in SA . (Nseq . (Nseq1 . k0)) & sb . (Nseq . (Nseq1 . k0)) in SB . (Nseq . (Nseq1 . k0)) ) by A19;
A51: ( SA . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) & SB . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) ) by A42, XBOOLE_1:17;
A52: dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) <= abs ((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))) by A50, Th16;

A53: 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 A52, ABSVALUE:def 1;
then dist A,B <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A43, 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 A48, A49, XXREAL_0:2;
then A54: ((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 A47, A50, A51, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A54; :: thesis: verum

end;

suppose sb . (Nseq . (Nseq1 . k0)) <= sa . (Nseq . (Nseq1 . k0)) ; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0))

then A55: (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) >= 0 by XREAL_1:50;
abs ((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))) = abs ((sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0)))) by UNIFORM1:13;
then dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A52, A55, ABSVALUE:def 1;
then dist A,B <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A43, 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 A48, A49, XXREAL_0:2;
then A56: ((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 A47, A50, A51, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A56; :: thesis: verum

end;

end;

end;

per cases ( ((lim (ga * Nseq1)) + (lim fb)) / 2 in B or ((lim (ga * Nseq1)) + (lim fb)) / 2 in A ) by A39, XBOOLE_0:def 3;

suppose A57: ((lim (ga * Nseq1)) + (lim fb)) / 2 in B ; :: thesis: contradiction

((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 A58: 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;
A59: 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 ;
(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 A40, XREAL_1:8;
then A60: abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((abs (((ga * Nseq1) . k0) - (fb . k0))) / 2) + ((dist A,B) / 2) by A58, A59, XXREAL_0:2;
A61: (ga * Nseq1) . k0 in SA . (Nseq . (Nseq1 . k0)) by A19, A45;
SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B by A15;
then A62: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SB . (Nseq . (Nseq1 . k0)) by A53, A57, XBOOLE_0:def 4;
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 A19, A45, A46, A60;
then abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) by A44, XXREAL_0:2;
hence contradiction by A61, A62, Th16; :: thesis: verum

end;

suppose A63: ((lim (ga * Nseq1)) + (lim fb)) / 2 in A ; :: thesis: contradiction

(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 A64: 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;
A65: 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 ;
(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 A40, XREAL_1:8;
then A66: abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((abs ((fb . k0) - ((ga * Nseq1) . k0))) / 2) + ((dist A,B) / 2) by A64, A65, XXREAL_0:2;
A67: fb . k0 in SB . (Nseq . (Nseq1 . k0)) by A19, A46;
SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A by A14;
then A68: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SA . (Nseq . (Nseq1 . k0)) by A53, A63, XBOOLE_0:def 4;
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 A19, A45, A46 ;
then abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < dist (SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))) by A44, A66, XXREAL_0:2;
hence contradiction by A67, A68, Th16; :: thesis: verum

end;

end;

end;

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 ) ) )
thus ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.e,f.] by A24, A30, A32, 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 ) ) )
thus not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B by A38; :: 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 )
A69: i <= Nseq . i by SEQM_3:33;
X: dom Nseq = NAT by FUNCT_2:def 1;
Y: dom Nseq1 = NAT by FUNCT_2:def 1;
i <= Nseq1 . i by SEQM_3:33;
then Nseq . i <= Nseq . (Nseq1 . i) by X, VALUED_0:def 15;
then A70: i <= Nseq . (Nseq1 . i) by A69, XXREAL_0:2;
set k = max k0,i;
take j = Nseq . (Nseq1 . (max k0,i)); :: thesis: ( i <= j & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j )
i <= max k0,i by XXREAL_0:25;
then Nseq1 . i <= Nseq1 . (max k0,i) by Y, VALUED_0:def 15;
then Nseq . (Nseq1 . i) <= j by X, VALUED_0:def 15;
hence i <= j by A70, XXREAL_0:2; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j
((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 A71: abs (((((ga * Nseq1) . (max k0,i)) + (fb . (max k0,i))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist A,B) / 2 by A37, XXREAL_0:25;
set di = dist (SA . j),(SB . j);
( T . j meets A & T . j meets B ) by A13;
then ( (T . j) /\ A <> {} & (T . j) /\ B <> {} ) by XBOOLE_0:def 7;
then A72: ( not SA . j is empty & not SB . j is empty ) by A14, A15;
A73: ( SA . j = (T . j) /\ A & SB . j = (T . j) /\ B ) by A14, A15;
then ( SA . j c= A & SB . j c= B ) by XBOOLE_1:17;
then A74: dist A,B <= dist (SA . j),(SB . j) by A72, Th17;
A75: (ga * Nseq1) . (max k0,i) = ga . (Nseq1 . (max k0,i)) by FUNCT_2:21
.= sa . j by A25, FUNCT_2:21 ;
A76: fb . (max k0,i) = (sb * Nseq) . (Nseq1 . (max k0,i)) by A31, FUNCT_2:21
.= sb . j by FUNCT_2:21 ;
T . j is closed-interval by A13;
then consider a, b being Real such that
a <= b and
A77: T . j = [.a,b.] by INTEGRA1:def 1;
2 * ((dist A,B) / 2) = dist A,B ;
then A78: 2 * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < dist A,B by A71, A75, A76, XREAL_1:70;
A79: 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))) ;
A80: ( sa . j in SA . j & sb . j in SB . j ) by A19;
A81: ( SA . j c= T . j & SB . j c= T . j ) by A73, XBOOLE_1:17;
A82: dist (SA . j),(SB . j) <= abs ((sb . j) - (sa . j)) by A80, Th16;

A83: 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 A82, ABSVALUE:def 1;
then dist A,B <= (sb . j) - (sa . j) by A74, XXREAL_0:2;
then abs (((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sb . j) - (sa . j) by A78, A79, XXREAL_0:2;
then A84: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sa . j),(sb . j).] by RCOMP_1:9;
[.(sa . j),(sb . j).] c= T . j by A77, A80, A81, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A84; :: thesis: verum

end;

suppose sb . j <= sa . j ; :: thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j

then A85: (sa . j) - (sb . j) >= 0 by XREAL_1:50;
abs ((sb . j) - (sa . j)) = abs ((sa . j) - (sb . j)) by UNIFORM1:13;
then dist (SA . j),(SB . j) <= (sa . j) - (sb . j) by A82, A85, ABSVALUE:def 1;
then dist A,B <= (sa . j) - (sb . j) by A74, XXREAL_0:2;
then abs (((sb . j) + (sa . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sa . j) - (sb . j) by A78, A79, XXREAL_0:2;
then A86: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sb . j),(sa . j).] by RCOMP_1:9;
[.(sb . j),(sa . j).] c= T . j by A77, A80, A81, XXREAL_2:def 12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A86; :: thesis: verum

end;

end;

end;

T . j c= S . j by A13;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j by A83; :: thesis: verum