let X be RealNormSpace; :: thesis: for vseq being sequence of (DualSp X)
for x, y being Point of X st vseq # x is convergent & vseq # y is convergent holds
( vseq # (x + y) is convergent & lim (vseq # (x + y)) = (lim (vseq # x)) + (lim (vseq # y)) )
let vseq be sequence of (DualSp X); :: thesis: for x, y being Point of X st vseq # x is convergent & vseq # y is convergent holds
( vseq # (x + y) is convergent & lim (vseq # (x + y)) = (lim (vseq # x)) + (lim (vseq # y)) )
let x, y be Point of X; :: thesis: ( vseq # x is convergent & vseq # y is convergent implies ( vseq # (x + y) is convergent & lim (vseq # (x + y)) = (lim (vseq # x)) + (lim (vseq # y)) ) )
assume that
A1: vseq # x is convergent and
A2: vseq # y is convergent ; :: thesis: ( vseq # (x + y) is convergent & lim (vseq # (x + y)) = (lim (vseq # x)) + (lim (vseq # y)) )

A3: now :: thesis: for p0 being Real st 0 < p0 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y)))).| < p0

let p0 be Real; :: thesis: ( 0 < p0 implies ex n being Nat st
for m being Nat st n <= m holds
|.(((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y)))).| < p0 )
set p = p0 / 2;
assume A4: 0 < p0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y)))).| < p0
then consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.(((vseq # x) . m) - (lim (vseq # x))).| < (p0 / 2) / 2 by SEQ_2:def 7, A1;
consider n2 being Nat such that
A7: for m being Nat st n2 <= m holds
|.(((vseq # y) . m) - (lim (vseq # y))).| < (p0 / 2) / 2 by SEQ_2:def 7, A2, A4;
reconsider n = max (n1,n2) as Nat by XXREAL_0:def 10;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y)))).| < p0
A8: ( n1 <= n & n2 <= n ) by XXREAL_0:25;
let m be Nat; :: thesis: ( n <= m implies |.(((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y)))).| < p0 )
assume A9: n <= m ; :: thesis: |.(((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y)))).| < p0
then n1 <= m by XXREAL_0:2, A8;
then A10: |.(((vseq # x) . m) - (lim (vseq # x))).| < (p0 / 2) / 2 by A6;
n2 <= m by A9, XXREAL_0:2, A8;
then A11: |.(((vseq # y) . m) - (lim (vseq # y))).| < (p0 / 2) / 2 by A7;
reconsider vseqm = vseq . m as Lipschitzian linear-Functional of X by DUALSP01:def 10;
(vseq # (x + y)) . m = vseqm . (x + y) by DUALSP03:def 1
.= ((vseq . m) . x) + ((vseq . m) . y) by HAHNBAN:def 2
.= ((vseq # x) . m) + ((vseq . m) . y) by DUALSP03:def 1
.= ((vseq # x) . m) + ((vseq # y) . m) by DUALSP03:def 1 ;
then ((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y))) = (((vseq # x) . m) - (lim (vseq # x))) + (((vseq # y) . m) - (lim (vseq # y))) ;
then A12: |.(((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y)))).| <= |.(((vseq # x) . m) - (lim (vseq # x))).| + |.(((vseq # y) . m) - (lim (vseq # y))).| by COMPLEX1:56;
|.(((vseq # x) . m) - (lim (vseq # x))).| + |.(((vseq # y) . m) - (lim (vseq # y))).| <= ((p0 / 2) / 2) + ((p0 / 2) / 2) by A10, A11, XREAL_1:7;
then A13: |.(((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y)))).| <= p0 / 2 by A12, XXREAL_0:2;
p0 / 2 < p0 by XREAL_1:216, A4;
hence |.(((vseq # (x + y)) . m) - ((lim (vseq # x)) + (lim (vseq # y)))).| < p0 by XXREAL_0:2, A13; :: thesis: verum

end;

hence vseq # (x + y) is convergent by SEQ_2:def 6; :: thesis: lim (vseq # (x + y)) = (lim (vseq # x)) + (lim (vseq # y))
hence lim (vseq # (x + y)) = (lim (vseq # x)) + (lim (vseq # y)) by SEQ_2:def 7, A3; :: thesis: verum