let p be Real; :: thesis: ( 0 < p implies for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| to_power p ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p ) )

assume A1: 0 < p ; :: thesis: for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| to_power p ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p )

let c be Real; :: thesis: for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| to_power p ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p )

let seq be Real_Sequence; :: thesis: ( seq is convergent implies for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| to_power p ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p ) )

assume A2: seq is convergent ; :: thesis: for rseq being Real_Sequence st ( for i being Nat holds rseq . i = |.((seq . i) - c).| to_power p ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p )

deffunc H1( set ) -> object = |.((seq . \$1) - c).|;
consider b being Real_Sequence such that
A3: for n being Nat holds b . n = H1(n) from SEQ_1:sch 1();
let rseq be Real_Sequence; :: thesis: ( ( for i being Nat holds rseq . i = |.((seq . i) - c).| to_power p ) implies ( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p ) )
assume A4: for i being Nat holds rseq . i = |.((seq . i) - c).| to_power p ; :: thesis: ( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p )
A5: for n being Nat holds rseq . n = (b . n) to_power p
proof
let n be Nat; :: thesis: rseq . n = (b . n) to_power p
rseq . n = |.((seq . n) - c).| to_power p by A4
.= (b . n) to_power p by A3 ;
hence rseq . n = (b . n) to_power p ; :: thesis: verum
end;
A6: for n being Nat holds 0 <= b . n
proof
let n be Nat; :: thesis: 0 <= b . n
b . n = |.((seq . n) - c).| by A3;
hence 0 <= b . n by COMPLEX1:46; :: thesis: verum
end;
A7: lim b = |.((lim seq) - c).| by ;
b is convergent by ;
hence ( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p ) by ; :: thesis: verum