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 H_{1}( set ) -> object = |.((seq . $1) - c).|;

consider b being Real_Sequence such that

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

b is convergent by A2, A3, RSSPACE3:1;

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

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 H

consider b being Real_Sequence such that

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

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

A6:
for n being Nat holds 0 <= b . n
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;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

proof

A7:
lim b = |.((lim seq) - c).|
by A2, A3, RSSPACE3:1;
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;b . n = |.((seq . n) - c).| by A3;

hence 0 <= b . n by COMPLEX1:46; :: thesis: verum

b is convergent by A2, A3, RSSPACE3:1;

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