for Sq0, Sq, Sq1 being Real_Sequence st Sq1 is convergent & ( for i being Nat holds
( Sq1 . (2 * i) = Sq0 . i & Sq1 . ((2 * i) + 1) = Sq . i ) ) holds
( Sq0 is convergent & lim Sq0 = lim Sq1 & Sq is convergent & lim Sq = lim Sq1 )