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

now

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

end;

then A8: rseq = b + seq1 by SEQ_1:11;
hence rseq is convergent by A3, A6, SEQ_2:19; :: thesis: lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1)
thus lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) by A3, A6, A7, A8, SEQ_2:20; :: thesis: verum