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 Nat holds rseq . i = (|.((seq . i) - c).| to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((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 Nat holds rseq . i = (|.((seq . i) - c).| to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((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 Nat holds rseq . i = (|.((seq . i) - c).| to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((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 Nat holds rseq . i = (|.((seq . i) - c).| to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((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 Nat holds rseq . i = (|.((seq . i) - c).| to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| to_power p) + (lim seq1) )
deffunc H₁( set ) -> object = |.((seq . $1) - c).| to_power p;
consider b being Real_Sequence such that
A4: for n being Nat holds b . n = H₁(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) + (seq1 . i) ) implies ( rseq is convergent & lim rseq = (|.((lim seq) - c).| to_power p) + (lim seq1) ) )
assume A5: for i being Nat holds rseq . i = (|.((seq . i) - c).| to_power p) + (seq1 . i) ; :: thesis: ( rseq is convergent & lim rseq = (|.((lim seq) - c).| to_power p) + (lim seq1) )

now :: thesis: for n being Nat holds rseq . n = (b . n) + (seq1 . n)

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

end;

then A6: rseq = b + seq1 by SEQ_1:7;
A7: b is convergent by A1, A2, A4, Lm8;
hence rseq is convergent by A3, A6, SEQ_2:5; :: thesis: lim rseq = (|.((lim seq) - c).| to_power p) + (lim seq1)
lim b = |.((lim seq) - c).| to_power p by A1, A2, A4, Lm8;
hence lim rseq = (|.((lim seq) - c).| to_power p) + (lim seq1) by A3, A7, A6, SEQ_2:6; :: thesis: verum