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

consider b being Real_Sequence such that

A4: 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) + (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) )

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

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

consider b being Real_Sequence such that

A4: 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) + (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)

then A6:
rseq = b + seq1
by SEQ_1:7;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;thus rseq . n = (|.((seq . n) - c).| to_power p) + (seq1 . n) by A5

.= (b . n) + (seq1 . n) by A4 ; :: thesis: verum

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