let Sq0, Sq, Sq1 be Real_Sequence; :: thesis:
assume that
A1: Sq1 is convergent and
A2: for i being Nat holds
( Sq1 . (2 * i) = Sq0 . i & Sq1 . ((2 * i) + 1) = Sq . i ) ; :: thesis:
A3: for r being Real st 0 < r holds
ex m1 being Nat st
for i being Nat st m1 <= i holds
|.((Sq0 . i) - (lim Sq1)).| < r

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider m being Nat such that
A4: for n being Nat st m <= n holds
|.((Sq1 . n) - (lim Sq1)).| < r by A1, SEQ_2:def 7;
consider k being Nat such that
A5: ( m = 2 * k or m = (2 * k) + 1 ) by INTEGR20:14;
(2 * k) + 1 <= ((2 * k) + 1) + 1 by NAT_1:11;
then A6: m <= (2 * k) + 2 by A5, XREAL_1:31;
reconsider m1 = k + 1 as Nat ;
take m1 ; :: thesis:
thus for i being Nat st m1 <= i holds
|.((Sq0 . i) - (lim Sq1)).| < r :: thesis:

let i be Nat; :: thesis:
assume m1 <= i ; :: thesis:
then 2 * m1 <= 2 * i by XREAL_1:64;
then m <= 2 * i by A6, XXREAL_0:2;
then |.((Sq1 . (2 * i)) - (lim Sq1)).| < r by A4;
hence |.((Sq0 . i) - (lim Sq1)).| < r by A2; :: thesis:

end;

hence Sq0 is convergent by SEQ_2:def 6; :: thesis:
hence lim Sq0 = lim Sq1 by A3, SEQ_2:def 7; :: thesis:
A7: for r being Real st 0 < r holds
ex m1 being Nat st
for i being Nat st m1 <= i holds
|.((Sq . i) - (lim Sq1)).| < r

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider m being Nat such that
A8: for n being Nat st m <= n holds
|.((Sq1 . n) - (lim Sq1)).| < r by A1, SEQ_2:def 7;
consider k being Nat such that
A9: ( m = 2 * k or m = (2 * k) + 1 ) by INTEGR20:14;
(2 * k) + 1 <= ((2 * k) + 1) + 1 by NAT_1:11;
then A10: m <= (2 * k) + 2 by A9, XREAL_1:31;
reconsider m1 = k + 1 as Nat ;
take m1 ; :: thesis:
thus for i being Nat st m1 <= i holds
|.((Sq . i) - (lim Sq1)).| < r :: thesis:

let i be Nat; :: thesis:
assume m1 <= i ; :: thesis:
then 2 * m1 <= 2 * i by XREAL_1:64;
then m <= 2 * i by A10, XXREAL_0:2;
then m <= (2 * i) + 1 by XREAL_1:145;
then |.((Sq1 . ((2 * i) + 1)) - (lim Sq1)).| < r by A8;
hence |.((Sq . i) - (lim Sq1)).| < r by A2; :: thesis:

end;