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 Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((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 Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((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 Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((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 Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p ) )
assume A2: seq is convergent ; :: thesis: for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p )
let rseq be Real_Sequence; :: thesis: ( ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ) implies ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p ) )
assume A3: for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) to_power p ; :: thesis: ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p )
deffunc H₁( set ) -> Element of REAL = abs ((seq . $1) - c);
consider b being Real_Sequence such that
A4: for n being Element of NAT holds b . n = H₁(n) from SEQ_1:sch 1();
A5: b is convergent by A2, A4, RSSPACE3:1;
A6: lim b = abs ((lim seq) - c) by A2, A4, RSSPACE3:1;
A7: for n being Element of NAT holds 0 <= b . n

proof

let n be Element of NAT ; :: thesis: 0 <= b . n
b . n = abs ((seq . n) - c) by A4;
hence 0 <= b . n by COMPLEX1:132; :: thesis: verum

end;

for n being Element of NAT holds rseq . n = (b . n) to_power p

proof

let n be Element of NAT ; :: thesis: rseq . n = (b . n) to_power p
rseq . n = (abs ((seq . n) - c)) to_power p by A3
.= (b . n) to_power p by A4 ;
hence rseq . n = (b . n) to_power p ; :: thesis: verum

end;

hence ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p ) by A1, A5, A6, A7, HOLDER_1:10; :: thesis: verum