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)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (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)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) ) )
assume that
A1: seq is convergent and
A2: seq1 is convergent ; :: thesis: for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )
reconsider cseq = NAT --> c as Real_Sequence ;
A3: seq - cseq is convergent by A1, SEQ_2:25;
then A4: abs (seq - cseq) is convergent by SEQ_4:26;
let rseq be Real_Sequence; :: thesis: ( ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) + (seq1 . i) ) implies ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) ) )
assume A5: for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) + (seq1 . i) ; :: thesis: ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )

now

let i be Element of NAT ; :: thesis: rseq . i = ((abs (seq - cseq)) + seq1) . i
thus rseq . i = (abs ((seq . i) - c)) + (seq1 . i) by A5
.= (abs ((seq . i) - (cseq . i))) + (seq1 . i) by FUNCOP_1:13
.= (abs ((seq . i) + (- (cseq . i)))) + (seq1 . i)
.= (abs ((seq . i) + ((- cseq) . i))) + (seq1 . i) by SEQ_1:14
.= (abs ((seq + (- cseq)) . i)) + (seq1 . i) by SEQ_1:11
.= (abs ((seq - cseq) . i)) + (seq1 . i) by SEQ_1:15
.= ((abs (seq - cseq)) . i) + (seq1 . i) by SEQ_1:16
.= ((abs (seq - cseq)) + seq1) . i by SEQ_1:11 ; :: thesis: verum

end;

then A6: rseq = (abs (seq - cseq)) + seq1 by FUNCT_2:113;
lim (abs (seq - cseq)) = abs (lim (seq - cseq)) by A3, SEQ_4:27
.= abs ((lim seq) - (lim cseq)) by A1, SEQ_2:26
.= abs ((lim seq) - (cseq . 0 )) by SEQ_4:41
.= abs ((lim seq) - c) by FUNCOP_1:13 ;
hence ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) ) by A2, A6, A4, SEQ_2:19, SEQ_2:20; :: thesis: verum