let seq, seq2 be Real_Sequence; :: thesis: for k being positive Real st seq is convergent & ( for n being Element of NAT holds seq2 . n = |.((lim seq) - (seq . n)).| to_power k ) holds
( seq2 is convergent & lim seq2 = 0 )
let k be positive Real; :: thesis: ( seq is convergent & ( for n being Element of NAT holds seq2 . n = |.((lim seq) - (seq . n)).| to_power k ) implies ( seq2 is convergent & lim seq2 = 0 ) )
set r = lim seq;
assume A1: ( seq is convergent & ( for n being Element of NAT holds seq2 . n = |.((lim seq) - (seq . n)).| to_power k ) ) ; :: thesis: ( seq2 is convergent & lim seq2 = 0 )
deffunc H₁( Element of NAT ) -> Element of REAL = |.((lim seq) - (seq . $1)).|;
consider seq1 being Real_Sequence such that
A2: for n being Element of NAT holds seq1 . n = H₁(n) from SEQ_1:sch 1();
deffunc H₂( Element of NAT ) -> Element of REAL = lim seq;
consider seq0 being Real_Sequence such that
A3: for n being Element of NAT holds seq0 . n = H₂(n) from SEQ_1:sch 1();
for n being Nat holds seq0 . n = lim seq

proof

let n be Nat; :: thesis: seq0 . n = lim seq
n in NAT by ORDINAL1:def 13;
hence seq0 . n = lim seq by A3; :: thesis: verum

end;

then A4: seq0 is constant by VALUED_0:def 18;
then A5: seq0 - seq is convergent by A1, SEQ_2:25;
A6: ( dom seq0 = NAT & dom seq = NAT & dom (seq0 - seq) = NAT & dom seq1 = NAT ) by FUNCT_2:def 1;
A7: dom (abs (seq0 - seq)) = dom (seq0 - seq) by VALUED_1:def 11;
for n being Element of NAT holds (abs (seq0 - seq)) . n = seq1 . n

proof

let n be Element of NAT ; :: thesis: (abs (seq0 - seq)) . n = seq1 . n
seq1 . n = |.((lim seq) - (seq . n)).| by A2;
then seq1 . n = |.((seq0 . n) - (seq . n)).| by A3;
then seq1 . n = abs ((seq0 - seq) . n) by A6, VALUED_1:13;
hence (abs (seq0 - seq)) . n = seq1 . n by A6, A7, VALUED_1:def 11; :: thesis: verum

end;

then A8: abs (seq0 - seq) = seq1 by FUNCT_2:113;
then A9: seq1 is convergent by A5, SEQ_4:26;
lim (seq0 - seq) = (seq0 . 0) - (lim seq) by A4, A1, SEQ_4:59;
then lim (seq0 - seq) = (lim seq) - (lim seq) by A3;
then A10: lim seq1 = 0 by A5, A8, COMPLEX1:130, SEQ_4:27;
for n being Element of NAT holds
( seq2 . n = (seq1 . n) to_power k & seq1 . n >= 0 )

proof

let n be Element of NAT ; :: thesis: ( seq2 . n = (seq1 . n) to_power k & seq1 . n >= 0 )
|.((lim seq) - (seq . n)).| = seq1 . n by A2;
hence ( seq2 . n = (seq1 . n) to_power k & seq1 . n >= 0 ) by A1, COMPLEX1:132; :: thesis: verum

end;

then ( seq2 is convergent & lim seq2 = (lim seq1) to_power k ) by A9, HOLDER_1:10;
hence ( seq2 is convergent & lim seq2 = 0 ) by A10, POWER:def 2; :: thesis: verum