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_{1}( Nat) -> object = |.((lim seq) - (seq . $1)).|;

consider seq1 being Real_Sequence such that

A2: for n being Nat holds seq1 . n = H_{1}(n)
from SEQ_1:sch 1();

deffunc H_{2}( Nat) -> object = lim seq;

consider seq0 being Real_Sequence such that

A3: for n being Nat holds seq0 . n = H_{2}(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

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 )

hence ( seq2 is convergent & lim seq2 = 0 ) by A10, POWER:def 2; :: thesis: verum

( 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

consider seq1 being Real_Sequence such that

A2: for n being Nat holds seq1 . n = H

deffunc H

consider seq0 being Real_Sequence such that

A3: for n being Nat holds seq0 . n = H

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

then A8:
abs (seq0 - seq) = seq1
by FUNCT_2:63;
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;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

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

then
( seq2 is convergent & lim seq2 = (lim seq1) to_power k )
by A9, HOLDER_1:10;
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;|.(r - (seq . n)).| = seq1 . n by A2;

hence ( seq2 . n = (seq1 . n) to_power k & seq1 . n >= 0 ) by A1, COMPLEX1:46; :: thesis: verum

hence ( seq2 is convergent & lim seq2 = 0 ) by A10, POWER:def 2; :: thesis: verum