let X be RealNormSpace; :: thesis: for X0 being Subset of X
for vseq being sequence of (DualSp X) st ( for x being Point of X st x in X0 holds
vseq # x is convergent ) holds
for x being Point of X st x in Lin X0 holds
vseq # x is convergent
let X0 be Subset of X; :: thesis: for vseq being sequence of (DualSp X) st ( for x being Point of X st x in X0 holds
vseq # x is convergent ) holds
for x being Point of X st x in Lin X0 holds
vseq # x is convergent
let vseq be sequence of (DualSp X); :: thesis: ( ( for x being Point of X st x in X0 holds
vseq # x is convergent ) implies for x being Point of X st x in Lin X0 holds
vseq # x is convergent )
assume A1: for x being Point of X st x in X0 holds
vseq # x is convergent ; :: thesis: for x being Point of X st x in Lin X0 holds
vseq # x is convergent
defpred S₁[ Nat] means for x being Point of X
for X1 being Subset of X
for L being Linear_Combination of X1 st X1 c= X0 & card (Carrier L) <= $1 & x in Lin X1 & x = Sum L holds
vseq # x is convergent ;
A2: S₁[ 0 ]

proof

let x be Point of X; :: thesis: for X1 being Subset of X
for L being Linear_Combination of X1 st X1 c= X0 & card (Carrier L) <= 0 & x in Lin X1 & x = Sum L holds
vseq # x is convergent
let X1 be Subset of X; :: thesis: for L being Linear_Combination of X1 st X1 c= X0 & card (Carrier L) <= 0 & x in Lin X1 & x = Sum L holds
vseq # x is convergent
let L be Linear_Combination of X1; :: thesis: ( X1 c= X0 & card (Carrier L) <= 0 & x in Lin X1 & x = Sum L implies vseq # x is convergent )
assume A3: ( X1 c= X0 & card (Carrier L) <= 0 & x in Lin X1 & x = Sum L ) ; :: thesis: vseq # x is convergent
Carrier L = {} by A3;
then A4: x = 0. X by A3, RLVECT_2:34;

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

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

end;

hence vseq # x is convergent by SEQ_2:def 6; :: thesis: verum

end;

A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
let x be Point of X; :: thesis: for X1 being Subset of X
for L being Linear_Combination of X1 st X1 c= X0 & card (Carrier L) <= k + 1 & x in Lin X1 & x = Sum L holds
vseq # x is convergent
let X1 be Subset of X; :: thesis: for L being Linear_Combination of X1 st X1 c= X0 & card (Carrier L) <= k + 1 & x in Lin X1 & x = Sum L holds
vseq # x is convergent
let L be Linear_Combination of X1; :: thesis: ( X1 c= X0 & card (Carrier L) <= k + 1 & x in Lin X1 & x = Sum L implies vseq # x is convergent )
assume A8: ( X1 c= X0 & card (Carrier L) <= k + 1 & x in Lin X1 & x = Sum L ) ; :: thesis: vseq # x is convergent

per cases ( Carrier L = {} or Carrier L <> {} ) ;

suppose Carrier L = {} ; :: thesis: vseq # x is convergent

then A10: x = 0. X by A8, RLVECT_2:34;

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

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

end;

hence vseq # x is convergent by SEQ_2:def 6; :: thesis: verum

end;

suppose Carrier L <> {} ; :: thesis: vseq # x is convergent

then consider v being object such that
A13: v in Carrier L by XBOOLE_0:def 1;
reconsider v = v as Point of X by A13;
A15P: Carrier L c= X1 by RLVECT_2:def 6;
reconsider X2 = X1 \ {v} as Subset of X ;
reconsider X3 = {v} as Subset of X ;
X2 c= X1 by XBOOLE_1:36;
then A18: X2 c= X0 by A8;
X1 = X2 \/ X3 by XBOOLE_1:45, A15P, A13, ZFMISC_1:31;
then consider L1 being Linear_Combination of X2, L2 being Linear_Combination of X3 such that
A19: ( Carrier L = (Carrier L1) \/ (Carrier L2) & L = L1 + L2 & Carrier L1 = (Carrier L) \ X3 & Carrier L2 = (Carrier L) \ X2 ) by NORMSP_4:8, XBOOLE_1:79;
A20: Sum L = (Sum L1) + (Sum L2) by A19, RLVECT_3:1;
A21: Sum L2 = (L2 . v) * v by RLVECT_2:32;
vseq # v is convergent by A1, A8, A13, A15P;
then A22: vseq # (Sum L2) is convergent by A21, Th2;
not v in Carrier L1

proof

assume v in Carrier L1 ; :: thesis: contradiction
then ( v in Carrier L & not v in {v} ) by A19, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then A24: Carrier L1 c< Carrier L by A19, XBOOLE_1:7, XBOOLE_0:def 8, A13;
A25P: card (Carrier L1) < k + 1 by A8, XXREAL_0:2, CARD_2:48, A24;
Sum L1 in Lin X2 by RLVECT_3:14;
then vseq # (Sum L1) is convergent by A7, A25P, A18, NAT_1:13;
hence vseq # x is convergent by Th1, A8, A20, A22; :: thesis: verum

end;

end;

end;

A27: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A6);
let x be Point of X; :: thesis: ( x in Lin X0 implies vseq # x is convergent )
assume A28: x in Lin X0 ; :: thesis: vseq # x is convergent
then consider l being Linear_Combination of X0 such that
A29: x = Sum l by RLVECT_3:14;
(card (Carrier l)) + 0 <= (card (Carrier l)) + 1 by XREAL_1:7;
hence vseq # x is convergent by A28, A29, A27; :: thesis: verum