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 A1: ( 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 ) ) ) ; :: thesis: ( d is convergent & lim d = lim a )

A2: now

let r be real number ; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((d . m) - (lim a)) < r )
assume A3: 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((d . m) - (lim a)) < r
then consider k1 being Element of NAT such that
A4: for m being Element of NAT st k1 <= m holds
abs ((a . m) - (lim a)) < r by A1, SEQ_2:def 7;
consider k2 being Element of NAT such that
A5: for m being Element of NAT st k2 <= m holds
abs ((b . m) - (lim b)) < r by A1, A3, SEQ_2:def 7;
take n = max (2 * k1),((2 * k2) + 1); :: thesis: for m being Element of NAT st n <= m holds
abs ((d . m) - (lim a)) < r
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((d . m) - (lim a)) < r )
assume n <= m ; :: thesis: abs ((d . m) - (lim a)) < r
then A6: ( 2 * k1 <= m & (2 * k2) + 1 <= m ) by XXREAL_0:30;
consider n being Element of NAT such that
A7: ( m = 2 * n or m = (2 * n) + 1 ) by SCHEME1:1;

now

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

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

then A9: abs ((d . m) - (lim a)) = abs ((a . n) - (lim a)) by A1;
n >= k1 by A6, A8, XREAL_1:70;
hence abs ((d . m) - (lim a)) < r by A4, A9; :: thesis: verum

end;

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

then A11: abs ((d . m) - (lim a)) = abs ((b . n) - (lim a)) by A1;

now

assume n < k2 ; :: thesis: contradiction
then 2 * n < 2 * k2 by XREAL_1:70;
hence contradiction by A6, A10, XREAL_1:8; :: thesis: verum

end;

hence abs ((d . m) - (lim a)) < r by A1, A5, A11; :: thesis: verum

end;

end;

end;

hence abs ((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 A2, SEQ_2:def 7; :: thesis: verum