let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for A being Subset of V st 0. GF <> 1. GF holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for A being Subset of V st 0. GF <> 1. GF holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )

let A be Subset of V; :: thesis: ( 0. GF <> 1. GF implies ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) )
assume A1: 0. GF <> 1. GF ; :: thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
thus ( A <> {} & A is linearly-closed implies for l being Linear_Combination of A holds Sum l in A ) :: thesis: ( ( for l being Linear_Combination of A holds Sum l in A ) implies ( A <> {} & A is linearly-closed ) )
proof
defpred S1[ Nat] means for l being Linear_Combination of A st card () = \$1 holds
Sum l in A;
assume that
A2: A <> {} and
A3: A is linearly-closed ; :: thesis: for l being Linear_Combination of A holds Sum l in A
A4: S1[ 0 ]
proof
let l be Linear_Combination of A; :: thesis: ( card () = 0 implies Sum l in A )
assume card () = 0 ; :: thesis: Sum l in A
then Carrier l = {} ;
then l = ZeroLC V by Def3;
then Sum l = 0. V by Lm1;
hence Sum l in A by ; :: thesis: verum
end;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
let l be Linear_Combination of A; :: thesis: ( card () = k + 1 implies Sum l in A )
deffunc H1( Element of V) -> Element of the carrier of GF = l . \$1;
consider F being FinSequence of V such that
A7: F is one-to-one and
A8: rng F = Carrier l and
A9: Sum l = Sum (l (#) F) by Def6;
reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;
assume A10: card () = k + 1 ; :: thesis: Sum l in A
then A11: len F = k + 1 by ;
then A12: len (l (#) F) = k + 1 by Def5;
A13: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A14: k + 1 in dom F by ;
k + 1 in dom F by ;
then reconsider v = F . (k + 1) as Element of V by FINSEQ_2:11;
consider f being Function of the carrier of V, the carrier of GF such that
A15: f . v = 0. GF and
A16: for u being Element of V st u <> v holds
f . u = H1(u) from reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
A17: v in Carrier l by ;
now :: thesis: for u being Element of V st not u in Carrier l holds
f . u = 0. GF
let u be Element of V; :: thesis: ( not u in Carrier l implies f . u = 0. GF )
assume A18: not u in Carrier l ; :: thesis: f . u = 0. GF
hence f . u = l . u by
.= 0. GF by A18 ;
:: thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def1;
A19: A \ {v} c= A by XBOOLE_1:36;
A20: Carrier l c= A by Def4;
then A21: (l . v) * v in A by ;
A22: Carrier f = () \ {v}
proof
thus Carrier f c= () \ {v} :: according to XBOOLE_0:def 10 :: thesis: () \ {v} c= Carrier f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in () \ {v} )
assume x in Carrier f ; :: thesis: x in () \ {v}
then consider u being Element of V such that
A23: u = x and
A24: f . u <> 0. GF ;
f . u = l . u by ;
then A25: x in Carrier l by ;
not x in {v} by ;
hence x in () \ {v} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in () \ {v} or x in Carrier f )
assume A26: x in () \ {v} ; :: thesis:
then x in Carrier l by XBOOLE_0:def 5;
then consider u being Element of V such that
A27: x = u and
A28: l . u <> 0. GF ;
not x in {v} by ;
then x <> v by TARSKI:def 1;
then l . u = f . u by ;
hence x in Carrier f by ; :: thesis: verum
end;
then Carrier f c= A \ {v} by ;
then Carrier f c= A by A19;
then reconsider f = f as Linear_Combination of A by Def4;
A29: len G = k by ;
then A30: len (f (#) G) = k by Def5;
A31: 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: ( not x in rng G or x in Carrier f )
assume x in rng G ; :: thesis:
then consider y being object such that
A32: y in dom G and
A33: G . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by ;
A34: ( dom G c= dom F & G . y = F . y ) by ;
then A37: not x in {v} by TARSKI:def 1;
x in rng F by ;
hence x in Carrier f by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in rng G )
assume A38: x in Carrier f ; :: thesis: x in rng G
then x in rng F by ;
then consider y being object such that
A39: y in dom F and
A40: F . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by ;
then y in (dom F) /\ (Seg k) by ;
then A41: y in dom G by RELAT_1:61;
then G . y = F . y by FUNCT_1:47;
hence x in rng G by ; :: thesis: verum
end;
(Seg (k + 1)) /\ (Seg k) = Seg k by
.= dom (f (#) G) by ;
then A42: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by ;
now :: thesis: for x being object st x in dom (f (#) G) holds
(f (#) G) . x = (l (#) F) . x
let x be object ; :: thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x )
A43: rng F c= the carrier of V by FINSEQ_1:def 4;
assume A44: x in dom (f (#) G) ; :: thesis: (f (#) G) . x = (l (#) F) . x
then reconsider n = x as Element of NAT by FINSEQ_3:23;
n in dom (l (#) F) by ;
then A45: n in dom F by ;
then F . n in rng F by FUNCT_1:def 3;
then reconsider w = F . n as Element of V by A43;
A46: n in dom G by ;
then A47: G . n in rng G by FUNCT_1:def 3;
rng G c= the carrier of V by FINSEQ_1:def 4;
then reconsider u = G . n as Element of V by A47;
not u in {v} by ;
then A48: u <> v by TARSKI:def 1;
A49: (f (#) G) . n = (f . u) * u by
.= (l . u) * u by ;
w = u by ;
hence (f (#) G) . x = (l (#) F) . x by ; :: thesis: verum
end;
then f (#) G = (l (#) F) | (Seg k) by ;
then A50: f (#) G = (l (#) F) | (dom (f (#) G)) by ;
v in rng F by ;
then {v} c= Carrier l by ;
then card () = (k + 1) - () by
.= (k + 1) - 1 by CARD_1:30
.= k by XCMPLX_1:26 ;
then A51: Sum f in A by A6;
G is one-to-one by ;
then A52: Sum (f (#) G) = Sum f by ;
(l (#) F) . (len F) = (l . v) * v by ;
then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by ;
hence Sum l in A by A3, A9, A21, A52, A51; :: thesis: verum
end;
let l be Linear_Combination of A; :: thesis: Sum l in A
A53: card () = card () ;
for k being Nat holds S1[k] from NAT_1:sch 2(A4, A5);
hence Sum l in A by A53; :: thesis: verum
end;
assume A54: for l being Linear_Combination of A holds Sum l in A ; :: thesis: ( A <> {} & A is linearly-closed )
hence A <> {} ; :: thesis:
( ZeroLC V is Linear_Combination of A & Sum () = 0. V ) by ;
then A55: 0. V in A by A54;
A56: for a being Element of GF
for v being Element of V st v in A holds
a * v in A
proof
let a be Element of GF; :: thesis: for v being Element of V st v in A holds
a * v in A

let v be Element of V; :: thesis: ( v in A implies a * v in A )
assume A57: v in A ; :: thesis: a * v in A
now :: thesis: a * v in A
per cases ( a = 0. GF or a <> 0. GF ) ;
suppose a = 0. GF ; :: thesis: a * v in A
hence a * v in A by ; :: thesis: verum
end;
suppose A58: a <> 0. GF ; :: thesis: a * v in A
deffunc H1( set ) -> Element of the carrier of GF = 0. GF;
consider f being Function of V,GF such that
A59: f . v = a and
A60: for u being Element of V st u <> v holds
f . u = H1(u) from reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now :: thesis: for u being Element of V st not u in {v} holds
f . u = 0. GF
let u be Element of V; :: thesis: ( not u in {v} implies f . u = 0. GF )
assume not u in {v} ; :: thesis: f . u = 0. GF
then u <> v by TARSKI:def 1;
hence f . u = 0. GF by A60; :: thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def1;
A61: Carrier f = {v}
proof
thus Carrier f c= {v} :: according to XBOOLE_0:def 10 :: thesis:
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v} )
assume x in Carrier f ; :: thesis: x in {v}
then consider u being Element of V such that
A62: x = u and
A63: f . u <> 0. GF ;
u = v by ;
hence x in {v} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v} or x in Carrier f )
assume x in {v} ; :: thesis:
then x = v by TARSKI:def 1;
hence x in Carrier f by ; :: thesis: verum
end;
{v} c= A by ;
then reconsider f = f as Linear_Combination of A by ;
consider F being FinSequence of V such that
A64: ( F is one-to-one & rng F = Carrier f ) and
A65: Sum (f (#) F) = Sum f by Def6;
F = <*v*> by ;
then f (#) F = <*((f . v) * v)*> by Th10;
then Sum f = a * v by ;
hence a * v in A by A54; :: thesis: verum
end;
end;
end;
hence a * v in A ; :: thesis: verum
end;
thus for v, u being Element of V st v in A & u in A holds
v + u in A :: according to VECTSP_4:def 1 :: thesis: for b1 being Element of the carrier of GF
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A )
proof
let v, u be Element of V; :: thesis: ( v in A & u in A implies v + u in A )
assume that
A66: v in A and
A67: u in A ; :: thesis: v + u in A
now :: thesis: v + u in A
per cases ( u = v or v <> u ) ;
suppose u = v ; :: thesis: v + u in A
then v + u = ((1. GF) * v) + v by VECTSP_1:def 17
.= ((1. GF) * v) + ((1. GF) * v) by VECTSP_1:def 17
.= ((1. GF) + (1. GF)) * v by VECTSP_1:def 15 ;
hence v + u in A by ; :: thesis: verum
end;
suppose A68: v <> u ; :: thesis: v + u in A
deffunc H1( set ) -> Element of the carrier of GF = 0. GF;
consider f being Function of V,GF such that
A69: ( f . v = 1. GF & f . u = 1. GF ) and
A70: for w being Element of V st w <> v & w <> u holds
f . w = H1(w) from reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now :: thesis: for w being Element of V st not w in {v,u} holds
f . w = 0. GF
let w be Element of V; :: thesis: ( not w in {v,u} implies f . w = 0. GF )
assume not w in {v,u} ; :: thesis: f . w = 0. GF
then ( w <> v & w <> u ) by TARSKI:def 2;
hence f . w = 0. GF by A70; :: thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def1;
A71: Carrier f = {v,u}
proof
thus Carrier f c= {v,u} :: according to XBOOLE_0:def 10 :: thesis: {v,u} c= Carrier f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v,u} )
assume x in Carrier f ; :: thesis: x in {v,u}
then ex w being Element of V st
( x = w & f . w <> 0. GF ) ;
then ( x = v or x = u ) by A70;
hence x in {v,u} by TARSKI:def 2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v,u} or x in Carrier f )
assume x in {v,u} ; :: thesis:
then ( x = v or x = u ) by TARSKI:def 2;
hence x in Carrier f by ; :: thesis: verum
end;
then A72: Carrier f c= A by ;
A73: ( (1. GF) * u = u & (1. GF) * v = v ) by VECTSP_1:def 17;
reconsider f = f as Linear_Combination of A by ;
consider F being FinSequence of V such that
A74: ( F is one-to-one & rng F = Carrier f ) and
A75: Sum (f (#) F) = Sum f by Def6;
( F = <*v,u*> or F = <*u,v*> ) by ;
then ( f (#) F = <*((1. GF) * v),((1. GF) * u)*> or f (#) F = <*((1. GF) * u),((1. GF) * v)*> ) by ;
then Sum f = v + u by ;
hence v + u in A by A54; :: thesis: verum
end;
end;
end;
hence v + u in A ; :: thesis: verum
end;
thus for b1 being Element of the carrier of GF
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A ) by A56; :: thesis: verum