let CNS be ComplexNormSpace; :: thesis: for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
lim (S1 + S2) = (lim S1) + (lim S2)
let S1, S2 be sequence of CNS; :: thesis: ( S1 is convergent & S2 is convergent implies lim (S1 + S2) = (lim S1) + (lim S2) )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; :: thesis: lim (S1 + S2) = (lim S1) + (lim S2)
set g2 = lim S2;
set g1 = lim S1;
set g = (lim S1) + (lim S2);
A3: now :: thesis: for r being Real st 0 < r holds
ex k being set st
for n being Nat st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
let r be Real; :: thesis: ( 0 < r implies ex k being set st
for n being Nat st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r )
assume A4: 0 < r ; :: thesis: ex k being set st
for n being Nat st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
then consider m1 being Nat such that
A5: for n being Nat st m1 <= n holds
||.((S1 . n) - (lim S1)).|| < r / 2 by A1, Def16;
consider m2 being Nat such that
A6: for n being Nat st m2 <= n holds
||.((S2 . n) - (lim S2)).|| < r / 2 by A2, A4, Def16;
take k = m1 + m2; :: thesis: for n being Nat st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
let n be Nat; :: thesis: ( k <= n implies ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r )
assume A7: k <= n ; :: thesis: ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
m2 <= k by NAT_1:12;
then m2 <= n by A7, XXREAL_0:2;
then A8: ||.((S2 . n) - (lim S2)).|| < r / 2 by A6;
A9: ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| = ||.((- ((lim S1) + (lim S2))) + ((S1 . n) + (S2 . n))).|| by NORMSP_1:def 2
.= ||.(((- (lim S1)) + (- (lim S2))) + ((S1 . n) + (S2 . n))).|| by RLVECT_1:31
.= ||.(((S1 . n) + ((- (lim S1)) + (- (lim S2)))) + (S2 . n)).|| by RLVECT_1:def 3
.= ||.((((S1 . n) - (lim S1)) + (- (lim S2))) + (S2 . n)).|| by RLVECT_1:def 3
.= ||.(((S1 . n) - (lim S1)) + ((S2 . n) - (lim S2))).|| by RLVECT_1:def 3 ;
A10: ||.(((S1 . n) - (lim S1)) + ((S2 . n) - (lim S2))).|| <= ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| by Def13;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A7, XXREAL_0:2;
then ||.((S1 . n) - (lim S1)).|| < r / 2 by A5;
then ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r by A9, A10, XXREAL_0:2; :: thesis: verum
end;
S1 + S2 is convergent by A1, A2, Th113;
hence lim (S1 + S2) = (lim S1) + (lim S2) by A3, Def16; :: thesis: verum