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).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((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 Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((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 Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
reconsider cc = c as Element of REAL by XREAL_0:def 1;
set cseq = seq_const c;
A3: seq - (seq_const c) is convergent by A1;
then A4: abs (seq - (seq_const c)) is convergent ;
let rseq be Real_Sequence; :: thesis: ( ( for i being Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) implies ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) ) )
assume A5: for i being Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ; :: thesis: ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )

now :: thesis: for i being Element of NAT holds rseq . i = ((abs (seq - (seq_const c))) + seq1) . i

let i be Element of NAT ; :: thesis: rseq . i = ((abs (seq - (seq_const c))) + seq1) . i
thus rseq . i = |.((seq . i) - c).| + (seq1 . i) by A5
.= |.((seq . i) - ((seq_const c) . i)).| + (seq1 . i) by SEQ_1:57
.= |.((seq . i) + (- ((seq_const c) . i))).| + (seq1 . i)
.= |.((seq . i) + ((- (seq_const c)) . i)).| + (seq1 . i) by SEQ_1:10
.= |.((seq + (- (seq_const c))) . i).| + (seq1 . i) by SEQ_1:7
.= |.((seq - (seq_const c)) . i).| + (seq1 . i) by SEQ_1:11
.= ((abs (seq - (seq_const c))) . i) + (seq1 . i) by SEQ_1:12
.= ((abs (seq - (seq_const c))) + seq1) . i by SEQ_1:7 ; :: thesis: verum

end;

then A6: rseq = (abs (seq - (seq_const c))) + seq1 by FUNCT_2:63;
lim (abs (seq - (seq_const c))) = |.(lim (seq - (seq_const c))).| by A3, SEQ_4:14
.= |.((lim seq) - (lim (seq_const c))).| by A1, SEQ_2:12
.= |.((lim seq) - ((seq_const c) . 0)).| by SEQ_4:26
.= |.((lim seq) - c).| by SEQ_1:57 ;
hence ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) ) by A2, A6, A4, SEQ_2:6; :: thesis: verum