let seq, seq2 be Real_Sequence; :: thesis: for k being positive Real st seq is convergent & ( for n being 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 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 Nat holds seq2 . n = |.((lim seq) - (seq . n)).| to_power k ) ) ; :: thesis: ( seq2 is convergent & lim seq2 = 0 )
deffunc H₁( Nat) -> object = |.((lim seq) - (seq . $1)).|;
consider seq1 being Real_Sequence such that
A2: for n being Nat holds seq1 . n = H₁(n) from SEQ_1:sch 1();
deffunc H₂( Nat) -> object = lim seq;
consider seq0 being Real_Sequence such that
A3: for n being Nat holds seq0 . n = H₂(n) from SEQ_1:sch 1();
reconsider r = lim seq as Element of REAL by XREAL_0:def 1;
for n being Nat holds seq0 . n = r by A3;
then A4: seq0 is constant by VALUED_0:def 18;
then A5: seq0 - seq is convergent by A1;
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 = |.(r - (seq . n)).| by A2;
then seq1 . n = |.((seq0 . n) - (seq . n)).| by A3;
then seq1 . n = |.((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:63;
then A9: seq1 is convergent by A5;
lim (seq0 - seq) = (seq0 . 0) - (lim seq) by A4, A1, SEQ_4:42;
then lim (seq0 - seq) = r - (lim seq) by A3;
then A10: lim seq1 = 0 by A5, A8, COMPLEX1:44, SEQ_4:14;
for n being Nat holds
( seq2 . n = (seq1 . n) to_power k & seq1 . n >= 0 )

proof

let n be Nat; :: thesis: ( seq2 . n = (seq1 . n) to_power k & seq1 . n >= 0 )
|.(r - (seq . n)).| = seq1 . n by A2;
hence ( seq2 . n = (seq1 . n) to_power k & seq1 . n >= 0 ) by A1, COMPLEX1:46; :: 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