let X be RealNormSpace; :: thesis: for vseq being sequence of (DualSp X)
for x being Point of X
for a being Real st vseq # x is convergent holds
( vseq # (a * x) is convergent & lim (vseq # (a * x)) = a * (lim (vseq # x)) )
let vseq be sequence of (DualSp X); :: thesis: for x being Point of X
for a being Real st vseq # x is convergent holds
( vseq # (a * x) is convergent & lim (vseq # (a * x)) = a * (lim (vseq # x)) )
let x be Point of X; :: thesis: for a being Real st vseq # x is convergent holds
( vseq # (a * x) is convergent & lim (vseq # (a * x)) = a * (lim (vseq # x)) )
let a be Real; :: thesis: ( vseq # x is convergent implies ( vseq # (a * x) is convergent & lim (vseq # (a * x)) = a * (lim (vseq # x)) ) )
assume A1: vseq # x is convergent ; :: thesis: ( vseq # (a * x) is convergent & lim (vseq # (a * x)) = a * (lim (vseq # x)) )

per cases ( a = 0 or a <> 0 ) ;

suppose A2: a = 0 ; :: thesis: ( vseq # (a * x) is convergent & lim (vseq # (a * x)) = a * (lim (vseq # x)) )

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

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p )
assume A4: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p
reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p )
assume n <= m ; :: thesis: |.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p
reconsider vseqm = vseq . m as Lipschitzian linear-Functional of X by DUALSP01:def 10;
(vseq # (a * x)) . m = (vseq . m) . (a * x) by DUALSP03:def 1
.= a * (vseqm . x) by HAHNBAN:def 3
.= 0 by A2 ;
hence |.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p by A4, A2; :: thesis: verum

end;

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

end;

suppose a <> 0 ; :: thesis: ( vseq # (a * x) is convergent & lim (vseq # (a * x)) = a * (lim (vseq # x)) )

then A5: 0 < |.a.| by COMPLEX1:47;

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

let p0 be Real; :: thesis: ( 0 < p0 implies ex n being Nat st
for m being Nat st n <= m holds
|.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p0 )
assume A7: 0 < p0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p0
set p = p0 / 2;
consider n being Nat such that
A8: for m being Nat st n <= m holds
|.(((vseq # x) . m) - (lim (vseq # x))).| < (p0 / 2) / |.a.| by SEQ_2:def 7, A1, A5, A7;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p0
let m be Nat; :: thesis: ( n <= m implies |.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p0 )
assume n <= m ; :: thesis: |.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p0
then A9: |.(((vseq # x) . m) - (lim (vseq # x))).| < (p0 / 2) / |.a.| by A8;
reconsider vseqm = vseq . m as Lipschitzian linear-Functional of X by DUALSP01:def 10;
(vseq # (a * x)) . m = (vseq . m) . (a * x) by DUALSP03:def 1
.= a * (vseqm . x) by HAHNBAN:def 3
.= a * ((vseq # x) . m) by DUALSP03:def 1 ;
then ((vseq # (a * x)) . m) - (a * (lim (vseq # x))) = a * (((vseq # x) . m) - (lim (vseq # x))) ;
then A10: |.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| = |.a.| * |.(((vseq # x) . m) - (lim (vseq # x))).| by COMPLEX1:65;
|.a.| * |.(((vseq # x) . m) - (lim (vseq # x))).| <= |.a.| * ((p0 / 2) / |.a.|) by A5, A9, XREAL_1:64;
then A11: |.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| <= p0 / 2 by A10, A5, XCMPLX_1:87;
p0 / 2 < p0 by XREAL_1:216, A7;
hence |.(((vseq # (a * x)) . m) - (a * (lim (vseq # x)))).| < p0 by XXREAL_0:2, A11; :: thesis: verum

end;

hence vseq # (a * x) is convergent by SEQ_2:def 6; :: thesis: lim (vseq # (a * x)) = a * (lim (vseq # x))
hence lim (vseq # (a * x)) = a * (lim (vseq # x)) by SEQ_2:def 7, A6; :: thesis: verum

end;

end;