let X be RealNormSpace; :: thesis: for Sq0, Sq, Sq1 being sequence of X 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 )
let Sq0, Sq, Sq1 be sequence of X; :: 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, NORMSP_1:def 7;
consider k being Nat such that
A5: ( m = 2 * k or m = (2 * k) + 1 ) by Th14;
(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 ; :: thesis: ( lim Sq0 = lim Sq1 & Sq is convergent & lim Sq = lim Sq1 )
hence lim Sq0 = lim Sq1 by A3, NORMSP_1: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, NORMSP_1:def 7;
consider k being Nat such that
A9: ( m = 2 * k or m = (2 * k) + 1 ) by Th14;
(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 ; :: thesis: lim Sq = lim Sq1
hence lim Sq = lim Sq1 by NORMSP_1:def 7, A7; :: thesis: verum