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

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 A6: 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
A7: 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
A8: for m being Element of NAT st k2 <= m holds
abs ((b . m) - (lim b)) < r by A2, A6, 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 A9: n <= m ; :: thesis: abs ((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

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

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

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

end;

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

A16: now

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;

abs ((d . m) - (lim a)) = abs ((b . n) - (lim a)) by A4, A15;
hence abs ((d . m) - (lim a)) < r by A3, A8, A16; :: 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 A5, SEQ_2:def 7; :: thesis: verum