let N be Nat; :: thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
lim (seq + seq9) = (lim seq) + (lim seq9)
let seq, seq9 be Real_Sequence of N; :: thesis: ( seq is convergent & seq9 is convergent implies lim (seq + seq9) = (lim seq) + (lim seq9) )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; :: thesis: lim (seq + seq9) = (lim seq) + (lim seq9)
A3: now :: thesis: for r being Real st 0 < r holds
ex k being set st
for m being Nat st k <= m holds
|.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r
let r be Real; :: thesis: ( 0 < r implies ex k being set st
for m being Nat st k <= m holds
|.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r )
assume 0 < r ; :: thesis: ex k being set st
for m being Nat st k <= m holds
|.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r
then A4: 0 < r / 2 by XREAL_1:215;
then consider n1 being Nat such that
A5: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < r / 2 by A1, Def9;
consider n2 being Nat such that
A6: for m being Nat st n2 <= m holds
|.((seq9 . m) - (lim seq9)).| < r / 2 by A2, A4, Def9;
take k = n1 + n2; :: thesis: for m being Nat st k <= m holds
|.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r
let m be Nat; :: thesis: ( k <= m implies |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r )
assume A7: k <= m ; :: thesis: |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r
n2 <= k by NAT_1:12;
then n2 <= m by A7, XXREAL_0:2;
then A8: |.((seq9 . m) - (lim seq9)).| < r / 2 by A6;
A9: |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| = |.((((seq + seq9) . m) - (lim seq)) - (lim seq9)).| by RLVECT_1:27
.= |.((((seq . m) + (seq9 . m)) - (lim seq)) - (lim seq9)).| by Th4
.= |.(((seq . m) + ((seq9 . m) - (lim seq))) - (lim seq9)).| by RLVECT_1:def 3
.= |.(((seq . m) + ((- (lim seq)) + (seq9 . m))) - (lim seq9)).|
.= |.((((seq . m) + (- (lim seq))) + (seq9 . m)) - (lim seq9)).| by RLVECT_1:def 3
.= |.((((seq . m) - (lim seq)) + (seq9 . m)) - (lim seq9)).|
.= |.(((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))).| by RLVECT_1:def 3 ;
A10: |.(((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))).| <= |.((seq . m) - (lim seq)).| + |.((seq9 . m) - (lim seq9)).| by Th29;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A7, XXREAL_0:2;
then |.((seq . m) - (lim seq)).| < r / 2 by A5;
then |.((seq . m) - (lim seq)).| + |.((seq9 . m) - (lim seq9)).| < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r by A9, A10, XXREAL_0:2; :: thesis: verum
end;
seq + seq9 is convergent by A1, A2, Th36;
hence lim (seq + seq9) = (lim seq) + (lim seq9) by A3, Def9; :: thesis: verum