let a, b, d be Real_Sequence; :: thesis: ( a is convergent & b is convergent & lim a = lim b & ( for n being Element of NAT holds
( d . (2 * n) = a . n & d . ((2 * n) + 1) = b . n ) ) implies ( d is convergent & lim d = lim a ) )
assume that
A1: a is convergent and
A2: b is convergent and
A3: lim a = lim b and
A4: for n being Element of NAT holds
( d . (2 * n) = a . n & d . ((2 * n) + 1) = b . n ) ; :: thesis: ( d is convergent & lim d = lim a )

A5: now :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((d . m) - (lim a)).| < r

let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.((d . m) - (lim a)).| < r )
assume A6: 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((d . m) - (lim a)).| < r
then consider k1 being Nat such that
A7: for m being Nat st k1 <= m holds
|.((a . m) - (lim a)).| < r by A1, SEQ_2:def 7;
consider k2 being Nat such that
A8: for m being Nat st k2 <= m holds
|.((b . m) - (lim b)).| < r by A2, A6, SEQ_2:def 7;
reconsider n = max ((2 * k1),((2 * k2) + 1)) as Nat by TARSKI:1;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((d . m) - (lim a)).| < r
let m be Nat; :: thesis: ( n <= m implies |.((d . m) - (lim a)).| < r )
assume A9: n <= m ; :: thesis: |.((d . m) - (lim a)).| < r
then A10: (2 * k2) + 1 <= m by XXREAL_0:30;
consider n being Element of NAT such that
A11: ( m = 2 * n or m = (2 * n) + 1 ) by SCHEME1:1;
A12: 2 * k1 <= m by A9, XXREAL_0:30;

now :: thesis: |.((d . m) - (lim a)).| < r

per cases ( m = 2 * n or m = (2 * n) + 1 ) by A11;

suppose A13: m = 2 * n ; :: thesis: |.((d . m) - (lim a)).| < r

then A14: n >= k1 by A12, XREAL_1:68;
|.((d . m) - (lim a)).| = |.((a . n) - (lim a)).| by A4, A13;
hence |.((d . m) - (lim a)).| < r by A7, A14; :: thesis: verum

end;

suppose A15: m = (2 * n) + 1 ; :: thesis: |.((d . m) - (lim a)).| < r

A16: now :: thesis: not n < k2

assume n < k2 ; :: thesis: contradiction
then 2 * n < 2 * k2 by XREAL_1:68;
hence contradiction by A10, A15, XREAL_1:6; :: thesis: verum

end;

|.((d . m) - (lim a)).| = |.((b . n) - (lim a)).| by A4, A15;
hence |.((d . m) - (lim a)).| < r by A3, A8, A16; :: thesis: verum

end;

end;

end;

hence |.((d . m) - (lim a)).| < r ; :: thesis: verum

end;

hence d is convergent by SEQ_2:def 6; :: thesis: lim d = lim a
hence lim d = lim a by A5, SEQ_2:def 7; :: thesis: verum