let RNS be RealNormSpace; :: thesis: for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
S1 + S2 is convergent
let S1, S2 be sequence of RNS; :: thesis: ( S1 is convergent & S2 is convergent implies S1 + S2 is convergent )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; :: thesis: S1 + S2 is convergent
consider g1 being Point of RNS such that
A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S1 . n) - g1).|| < r by A1, Def9;
consider g2 being Point of RNS such that
A4: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S2 . n) - g2).|| < r by A2, Def9;
take g = g1 + g2; :: according to NORMSP_1:def 6 :: thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 + S2) . n) - g).|| < r
let r be Real; :: thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 + S2) . n) - g).|| < r )
assume A5: 0 < r ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 + S2) . n) - g).|| < r
then consider m1 being Element of NAT such that
A6: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - g1).|| < r / 2 by A3, XREAL_1:215;
consider m2 being Element of NAT such that
A7: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - g2).|| < r / 2 by A4, A5, XREAL_1:215;
take k = m1 + m2; :: thesis: for n being Element of NAT st k <= n holds
||.(((S1 + S2) . n) - g).|| < r
let n be Element of NAT ; :: thesis: ( k <= n implies ||.(((S1 + S2) . n) - g).|| < r )
assume A8: k <= n ; :: thesis: ||.(((S1 + S2) . n) - g).|| < r
m2 <= k by NAT_1:12;
then m2 <= n by A8, XXREAL_0:2;
then A9: ||.((S2 . n) - g2).|| < r / 2 by A7;
A10: ||.(((S1 + S2) . n) - g).|| = ||.((- (g1 + g2)) + ((S1 . n) + (S2 . n))).|| by Def5
.= ||.(((- g1) + (- g2)) + ((S1 . n) + (S2 . n))).|| by RLVECT_1:31
.= ||.(((S1 . n) + ((- g1) + (- g2))) + (S2 . n)).|| by RLVECT_1:def 3
.= ||.((((S1 . n) - g1) + (- g2)) + (S2 . n)).|| by RLVECT_1:def 3
.= ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| by RLVECT_1:def 3 ;
A11: ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| <= ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| by Def2;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A8, XXREAL_0:2;
then ||.((S1 . n) - g1).|| < r / 2 by A6;
then ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| < (r / 2) + (r / 2) by A9, XREAL_1:8;
hence ||.(((S1 + S2) . n) - g).|| < r by A10, A11, XXREAL_0:2; :: thesis: verum