for a, b, d being Real_Sequence st 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 ) ) holds
( d is convergent & lim d = lim a )