let A be non empty closed_interval Subset of REAL; :: thesis: for T0, T, T1 being DivSequence of A st delta T0 is convergent & lim (delta T0) = 0 & delta T is convergent & lim (delta T) = 0 & ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
( delta T1 is convergent & lim (delta T1) = 0 )
let T0, T, T1 be DivSequence of A; :: thesis: ( delta T0 is convergent & lim (delta T0) = 0 & delta T is convergent & lim (delta T) = 0 & ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) implies ( delta T1 is convergent & lim (delta T1) = 0 ) )
assume that
A1: ( delta T0 is convergent & lim (delta T0) = 0 ) and
A2: ( delta T is convergent & lim (delta T) = 0 ) and
A3: for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ; :: thesis: ( delta T1 is convergent & lim (delta T1) = 0 )
A4: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((delta T1) . m) - 0).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((delta T1) . b5) - 0).| < b3 )
assume A5: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((delta T1) . b5) - 0).| < b3
then consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.(((delta T0) . m) - 0).| < p by A1, SEQ_2:def 7;
consider n2 being Nat such that
A7: for m being Nat st n2 <= m holds
|.(((delta T) . m) - 0).| < p by A5, A2, SEQ_2:def 7;
reconsider n3 = max (n1,n2) as Nat by TARSKI:1;
A8: ( n1 <= n3 & n2 <= n3 ) by XXREAL_0:25;
reconsider n = (2 * n3) + 1 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((delta T1) . b4) - 0).| < b2
let m be Nat; :: thesis: ( n <= m implies |.(((delta T1) . b3) - 0).| < b1 )
assume A9: n <= m ; :: thesis: |.(((delta T1) . b3) - 0).| < b1
consider k being Nat such that
A10: ( m = 2 * k or m = (2 * k) + 1 ) by Th14;
reconsider k1 = k, m1 = m as Element of NAT by ORDINAL1:def 12;
per cases ( m = 2 * k or m = (2 * k) + 1 ) by A10;
suppose A11: m = 2 * k ; :: thesis: |.(((delta T1) . b3) - 0).| < b1
(delta T1) . m1 = delta (T1 . m1) by INTEGRA3:def 2;
then (delta T1) . m1 = delta (T0 . k1) by A11, A3;
then A12: (delta T1) . m1 = (delta T0) . k1 by INTEGRA3:def 2;
A13: 2 * n3 <= (2 * k) - 1 by XREAL_1:19, A9, A11;
(2 * k) - 1 < ((2 * k) - 1) + 1 by XREAL_1:145;
then 2 * n3 <= 2 * k by A13, XXREAL_0:2;
then (2 * n3) / 2 <= (2 * k) / 2 by XREAL_1:72;
then n1 <= k by A8, XXREAL_0:2;
hence |.(((delta T1) . m) - 0).| < p by A12, A6; :: thesis: verum
end;
suppose A14: m = (2 * k) + 1 ; :: thesis: |.(((delta T1) . b3) - 0).| < b1
(delta T1) . m1 = delta (T1 . m1) by INTEGRA3:def 2;
then (delta T1) . m1 = delta (T . k1) by A14, A3;
then A15: (delta T1) . m1 = (delta T) . k1 by INTEGRA3:def 2;
((2 * n3) + 1) - 1 <= ((2 * k) + 1) - 1 by XREAL_1:13, A9, A14;
then (2 * n3) / 2 <= (2 * k) / 2 by XREAL_1:72;
then n2 <= k by A8, XXREAL_0:2;
hence |.(((delta T1) . m) - 0).| < p by A15, A7; :: thesis: verum
end;
end;
end;
hence delta T1 is convergent by SEQ_2:def 6; :: thesis: lim (delta T1) = 0
hence lim (delta T1) = 0 by A4, SEQ_2:def 7; :: thesis: verum