let seq, seq9 be Real_Sequence; :: thesis: ( seq is convergent & seq9 is convergent implies seq + seq9 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; :: thesis: seq + seq9 is convergent
consider g1 being real number such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by A1, Def6;
consider g2 being real number such that
A4: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq9 . m) - g2) < p by A2, Def6;
take g = g1 + g2; :: according to SEQ_2:def 6 :: thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq + seq9) . m) - g) < p
let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq + seq9) . m) - g) < p )
assume A5: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq + seq9) . m) - g) < p
then consider n1 being Element of NAT such that
A6: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p / 2 by A3, XREAL_1:215;
consider n2 being Element of NAT such that
A7: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - g2) < p / 2 by A4, A5, XREAL_1:215;
take k = n1 + n2; :: thesis: for m being Element of NAT st k <= m holds
abs (((seq + seq9) . m) - g) < p
let m be Element of NAT ; :: thesis: ( k <= m implies abs (((seq + seq9) . m) - g) < p )
assume A8: k <= m ; :: thesis: abs (((seq + seq9) . m) - g) < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A8, XXREAL_0:2;
then A9: abs ((seq . m) - g1) < p / 2 by A6;
n2 <= k by NAT_1:12;
then n2 <= m by A8, XXREAL_0:2;
then abs ((seq9 . m) - g2) < p / 2 by A7;
then A10: (abs ((seq . m) - g1)) + (abs ((seq9 . m) - g2)) < (p / 2) + (p / 2) by A9, XREAL_1:8;
A11: abs (((seq + seq9) . m) - g) = abs (((seq . m) + (seq9 . m)) - (g1 + g2)) by SEQ_1:7
.= abs (((seq . m) - g1) + ((seq9 . m) - g2)) ;
abs (((seq . m) - g1) + ((seq9 . m) - g2)) <= (abs ((seq . m) - g1)) + (abs ((seq9 . m) - g2)) by COMPLEX1:56;
hence abs (((seq + seq9) . m) - g) < p by A10, A11, XXREAL_0:2; :: thesis: verum