let V be ComplexLinearSpace; :: thesis:
let A be Subset of V; :: thesis:
assume A1: A <> {} ; :: thesis:
thus ( A is linearly-closed implies for l being C_Linear_Combination of A holds Sum l in A ) :: thesis:

proof

defpred S₁[ Nat] means for l being C_Linear_Combination of A st card (Carrier l) = $1 holds
Sum l in A;
assume A2: A is linearly-closed ; :: thesis:
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A4: S₁[k] ; :: thesis:

hereby :: thesis:

let l be C_Linear_Combination of A; :: thesis:
deffunc H₁( Element of V) -> Element of COMPLEX = l . $1;
consider F being FinSequence of the carrier of V such that
A5: F is one-to-one and
A6: rng F = Carrier l and
A7: Sum l = Sum (l (#) F) by Def6;
reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;
assume A8: card (Carrier l) = k + 1 ; :: thesis:
then A9: len F = k + 1 by A5, A6, FINSEQ_4:62;
then A10: len (l (#) F) = k + 1 by Def5;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A11: k + 1 in dom F by A9, FINSEQ_1:def 3;
then reconsider v = F . (k + 1) as VECTOR of V by FUNCT_1:102;
consider f being Function of the carrier of V,COMPLEX such that
A12: ( f . v = 0c & ( for u being Element of V st u <> v holds
f . u = H₁(u) ) ) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8;

now :: thesis:

let u be VECTOR of V; :: thesis:
assume not u in Carrier l ; :: thesis:
then l . u = 0c ;
hence f . u = 0c by A12; :: thesis:

end;

then reconsider f = f as C_Linear_Combination of V by Def1;
A13: Carrier f = (Carrier l) \ {v}

proof

now :: thesis:

let x be object ; :: thesis:
assume x in Carrier f ; :: thesis:
then A14: ex u being VECTOR of V st
( u = x & f . u <> 0c ) ;
then f . x = l . x by A12;
then A15: x in Carrier l by A14;
not x in {v} by A12, A14, TARSKI:def 1;
hence x in (Carrier l) \ {v} by A15, XBOOLE_0:def 5; :: thesis:

end;

hence Carrier f c= (Carrier l) \ {v} ; :: according to XBOOLE_0:def 10 :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A16: x in (Carrier l) \ {v} ; :: thesis:
then not x in {v} by XBOOLE_0:def 5;
then x <> v by TARSKI:def 1;
then A17: l . x = f . x by A12, A16;
x in Carrier l by A16, XBOOLE_0:def 5;
then ex u being VECTOR of V st
( x = u & l . u <> 0c ) ;
hence x in Carrier f by A17; :: thesis:

end;

A18: Carrier l c= A by Def4;
then Carrier f c= A \ {v} by A13, XBOOLE_1:33;
then Carrier f c= A by XBOOLE_1:106;
then reconsider f = f as C_Linear_Combination of A by Def4;
A19: len G = k by A9, FINSEQ_3:53;
then A20: len (f (#) G) = k by Def5;
A21: rng G = Carrier f

proof

thus rng G c= Carrier f :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng G ; :: thesis:
then consider y being object such that
A22: y in dom G and
A23: G . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A22;
A24: ( dom G c= dom F & G . y = F . y ) by A22, FUNCT_1:47, RELAT_1:60;
then ( x = v implies ( k + 1 = y & y <= k & k < k + 1 ) ) by A5, A19, A11, A22, A23, FINSEQ_3:25, FUNCT_1:def 4, XREAL_1:29;
then A25: not x in {v} by TARSKI:def 1;
x in rng F by A22, A23, A24, FUNCT_1:def 3;
hence x in Carrier f by A6, A13, A25, XBOOLE_0:def 5; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: x in Carrier f ; :: thesis:
then x in rng F by A6, A13, XBOOLE_0:def 5;
then consider y being object such that
A27: y in dom F and
A28: F . y = x by FUNCT_1:def 3;

now :: thesis:

assume not y in Seg k ; :: thesis:
then y in (dom F) \ (Seg k) by A27, XBOOLE_0:def 5;
then y in (Seg (k + 1)) \ (Seg k) by A9, FINSEQ_1:def 3;
then y in {(k + 1)} by FINSEQ_3:15;
then y = k + 1 by TARSKI:def 1;
then not v in {v} by A13, A26, A28, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

then y in (dom F) /\ (Seg k) by A27, XBOOLE_0:def 4;
then A29: y in dom G by RELAT_1:61;
then G . y = F . y by FUNCT_1:47;
hence x in rng G by A28, A29, FUNCT_1:def 3; :: thesis:

end;

(Seg (k + 1)) /\ (Seg k) = Seg k by FINSEQ_1:7, NAT_1:12
.= dom (f (#) G) by A20, FINSEQ_1:def 3 ;
then A30: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A10, FINSEQ_1:def 3;

now :: thesis:

let x be object ; :: thesis:
assume A31: x in dom (f (#) G) ; :: thesis:
then A32: x in dom G by A19, A20, FINSEQ_3:29;
then A33: G . x in rng G by FUNCT_1:def 3;
then reconsider u = G . x as VECTOR of V ;
A34: F . x = u by A32, FUNCT_1:47;
not u in {v} by A13, A21, A33, XBOOLE_0:def 5;
then A35: u <> v by TARSKI:def 1;
x in dom (l (#) F) by A30, A31, XBOOLE_0:def 4;
then A36: x in dom F by A9, A10, FINSEQ_3:29;
(f (#) G) . x = (f . u) * u by A32, Th6
.= (l . u) * u by A12, A35 ;
hence (f (#) G) . x = (l (#) F) . x by A36, A34, Th6; :: thesis:

end;

then A37: f (#) G = (l (#) F) | (Seg k) by A30, FUNCT_1:46;
v in rng F by A11, FUNCT_1:def 3;
then {v} c= Carrier l by A6, ZFMISC_1:31;
then card (Carrier f) = (k + 1) - (card {v}) by A8, A13, CARD_2:44;
then card (Carrier f) = (k + 1) - 1 by CARD_1:30;
then A38: Sum f in A by A4;
v in Carrier l by A6, A11, FUNCT_1:def 3;
then A39: (l . v) * v in A by A2, A18;
G is one-to-one by A5, FUNCT_1:52;
then A40: Sum (f (#) G) = Sum f by A21, Def6;
( dom (f (#) G) = Seg (len (f (#) G)) & (l (#) F) . (len F) = (l . v) * v ) by A9, A11, Th6, FINSEQ_1:def 3;
then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by A9, A10, A20, A37, RLVECT_1:38;
hence Sum l in A by A2, A7, A39, A40, A38; :: thesis:

end;

let l be C_Linear_Combination of A; :: thesis:
A41: card (Carrier l) = card (Carrier l) ;

now :: thesis:

let l be C_Linear_Combination of A; :: thesis:
assume card (Carrier l) = 0 ; :: thesis:
then Carrier l = {} ;
then l = ZeroCLC V by Def3;
then Sum l = 0. V by Th11;
hence Sum l in A by A1, A2, CLVECT_1:20; :: thesis:

end;

then A42: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A42, A3);
hence Sum l in A by A41; :: thesis:

end;

assume A43: for l being C_Linear_Combination of A holds Sum l in A ; :: thesis:
( ZeroCLC V is C_Linear_Combination of A & Sum (ZeroCLC V) = 0. V ) by Th4, Th11;
then A44: 0. V in A by A43;
A45: for a being Complex
for v being VECTOR of V st v in A holds
a * v in A

proof

let a be Complex; :: thesis:
let v be VECTOR of V; :: thesis:
assume A46: v in A ; :: thesis:

now :: thesis:

reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
deffunc H₁( Element of V) -> Element of COMPLEX = 0c ;
consider f being Function of the carrier of V,COMPLEX such that
A47: ( f . v = a1 & ( for u being Element of V st u <> v holds
f . u = H₁(u) ) ) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8;

now :: thesis:

let u be VECTOR of V; :: thesis:
assume not u in {v} ; :: thesis:
then u <> v by TARSKI:def 1;
hence f . u = 0 by A47; :: thesis:

end;

then reconsider f = f as C_Linear_Combination of V by Def1;
assume A48: a <> 0 ; :: thesis:
A49: Carrier f = {v}

proof

now :: thesis:

let x be object ; :: thesis:
assume x in Carrier f ; :: thesis:
then ex u being VECTOR of V st
( x = u & f . u <> 0 ) ;
then x = v by A47;
hence x in {v} by TARSKI:def 1; :: thesis:

end;

hence Carrier f c= {v} ; :: according to XBOOLE_0:def 10 :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {v} ; :: thesis:
then x = v by TARSKI:def 1;
hence x in Carrier f by A48, A47; :: thesis:

end;

{v} c= A by A46, ZFMISC_1:31;
then reconsider f = f as C_Linear_Combination of A by A49, Def4;
consider F being FinSequence of the carrier of V such that
A50: ( F is one-to-one & rng F = Carrier f ) and
A51: Sum (f (#) F) = Sum f by Def6;
F = <*v*> by A49, A50, FINSEQ_3:97;
then f (#) F = <*((f . v) * v)*> by Th8;
then Sum f = a * v by A47, A51, RLVECT_1:44;
hence a * v in A by A43; :: thesis:

end;

hence a * v in A by A44, CLVECT_1:1; :: thesis:

end;

for v, u being VECTOR of V st v in A & u in A holds
v + u in A

proof

let v, u be VECTOR of V; :: thesis:
assume that
A52: v in A and
A53: u in A ; :: thesis:
A54: 1r * v = v by CLVECT_1:def 5;
A55: 1r * u = u by CLVECT_1:def 5;

A56: now :: thesis:

deffunc H₁( Element of V) -> Element of COMPLEX = 0c ;
assume A57: v <> u ; :: thesis:
consider f being Function of the carrier of V,COMPLEX such that
A58: ( f . v = 1r & f . u = 1r ) and
A59: for w being Element of V st w <> v & w <> u holds
f . w = H₁(w) from FUNCT_2:sch 7(A57);
reconsider f = f as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8;

now :: thesis:

let w be VECTOR of V; :: thesis:
assume not w in {v,u} ; :: thesis:
then ( w <> v & w <> u ) by TARSKI:def 2;
hence f . w = 0 by A59; :: thesis:

end;

then reconsider f = f as C_Linear_Combination of V by Def1;
A60: Carrier f = {v,u}

proof

thus Carrier f c= {v,u} :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Carrier f ; :: thesis:
then ex w being VECTOR of V st
( x = w & f . w <> 0c ) ;
then ( x = v or x = u ) by A59;
hence x in {v,u} by TARSKI:def 2; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {v,u} ; :: thesis:
then ( x = v or x = u ) by TARSKI:def 2;
hence x in Carrier f by A58; :: thesis:

end;

then Carrier f c= A by A52, A53, ZFMISC_1:32;
then reconsider f = f as C_Linear_Combination of A by Def4;
consider F being FinSequence of the carrier of V such that
A61: ( F is one-to-one & rng F = Carrier f ) and
A62: Sum (f (#) F) = Sum f by Def6;
( F = <*v,u*> or F = <*u,v*> ) by A57, A60, A61, FINSEQ_3:99;
then ( f (#) F = <*(1r * v),(1r * u)*> or f (#) F = <*(1r * u),(1r * v)*> ) by A58, Th9;
then Sum f = v + u by A55, A54, A62, RLVECT_1:45;
hence v + u in A by A43; :: thesis:

end;

v + v = (1r + 1r) * v by A54, CLVECT_1:def 3;
hence v + u in A by A45, A52, A56; :: thesis:

end;

hence A is linearly-closed by A45; :: thesis: