let Sq0, Sq, Sq1 be Real_Sequence; :: thesis: ( Sq1 is convergent & ( for i being Nat holds
( Sq1 . (2 * i) = Sq0 . i & Sq1 . ((2 * i) + 1) = Sq . i ) ) implies ( Sq0 is convergent & lim Sq0 = lim Sq1 & Sq is convergent & lim Sq = lim Sq1 ) )
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: ( Sq0 is convergent & lim Sq0 = lim Sq1 & Sq is convergent & lim Sq = lim Sq1 )
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

proof

let r be Real; :: thesis: ( 0 < r implies ex m1 being Nat st
for i being Nat st m1 <= i holds
|.((Sq0 . i) - (lim Sq1)).| < r )
assume 0 < r ; :: thesis: ex m1 being Nat st
for i being Nat st m1 <= i holds
|.((Sq0 . i) - (lim Sq1)).| < r
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: for i being Nat st m1 <= i holds
|.((Sq0 . i) - (lim Sq1)).| < r
thus for i being Nat st m1 <= i holds
|.((Sq0 . i) - (lim Sq1)).| < r :: thesis: verum

proof

let i be Nat; :: thesis: ( m1 <= i implies |.((Sq0 . i) - (lim Sq1)).| < r )
assume m1 <= i ; :: thesis: |.((Sq0 . i) - (lim Sq1)).| < r
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: verum

end;

end;

hence Sq0 is convergent by SEQ_2:def 6; :: thesis: ( lim Sq0 = lim Sq1 & Sq is convergent & lim Sq = lim Sq1 )
hence lim Sq0 = lim Sq1 by A3, SEQ_2:def 7; :: thesis: ( Sq is convergent & lim Sq = lim Sq1 )
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

proof

let r be Real; :: thesis: ( 0 < r implies ex m1 being Nat st
for i being Nat st m1 <= i holds
|.((Sq . i) - (lim Sq1)).| < r )
assume 0 < r ; :: thesis: ex m1 being Nat st
for i being Nat st m1 <= i holds
|.((Sq . i) - (lim Sq1)).| < r
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: for i being Nat st m1 <= i holds
|.((Sq . i) - (lim Sq1)).| < r
thus for i being Nat st m1 <= i holds
|.((Sq . i) - (lim Sq1)).| < r :: thesis: verum

proof

let i be Nat; :: thesis: ( m1 <= i implies |.((Sq . i) - (lim Sq1)).| < r )
assume m1 <= i ; :: thesis: |.((Sq . i) - (lim Sq1)).| < r
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: verum

end;

end;

hence Sq is convergent by SEQ_2:def 6; :: thesis: lim Sq = lim Sq1
hence lim Sq = lim Sq1 by SEQ_2:def 7, A7; :: thesis: verum