let V be RealLinearSpace; :: thesis: for A being Subset of V
for x being set st x in Z_Lin A holds
ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) )
let A be Subset of V; :: thesis: for x being set st x in Z_Lin A holds
ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) )
let x be set ; :: thesis: ( x in Z_Lin A implies ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) ) )
assume x in Z_Lin A ; :: thesis: ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) )
then consider z being Linear_Combination of A such that
A1: ( x = Sum z & rng z c= INT ) ;
consider F being FinSequence of V such that
A2: ( F is one-to-one & rng F = Carrier z & Sum z = Sum (z (#) F) ) by RLVECT_2:def 8;
A3: ( len (z (#) F) = len F & ( for i being Nat st i in dom (z (#) F) holds
(z (#) F) . i = (z . (F /. i)) * (F /. i) ) ) by RLVECT_2:def 7;
defpred S₁[ Nat, set ] means $2 = z . (F /. $1);

A4: now :: thesis: for k being Nat st k in Seg (len F) holds
ex x being Element of INT st S₁[k,x]

let k be Nat; :: thesis: ( k in Seg (len F) implies ex x being Element of INT st S₁[k,x] )
assume k in Seg (len F) ; :: thesis: ex x being Element of INT st S₁[k,x]
z . (F /. k) in rng z by FUNCT_2:4;
hence ex x being Element of INT st S₁[k,x] by A1; :: thesis: verum

end;

consider u being FinSequence of INT such that
A5: ( dom u = Seg (len F) & ( for i being Nat st i in Seg (len F) holds
S₁[i,u . i] ) ) from FINSEQ_1:sch 5(A4);
A6: rng F c= A by A2, RLVECT_2:def 6;
A7: len F = len (z (#) F) by RLVECT_2:def 7;
A8: len F = len u by A5, FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in Seg (len F) holds
(z (#) F) /. i = (u . i) * (F /. i)

let i be Nat; :: thesis: ( i in Seg (len F) implies (z (#) F) /. i = (u . i) * (F /. i) )
assume A9: i in Seg (len F) ; :: thesis: (z (#) F) /. i = (u . i) * (F /. i)
then A10: i in dom (z (#) F) by A3, FINSEQ_1:def 3;
hence (z (#) F) /. i = (z (#) F) . i by PARTFUN1:def 6
.= (z . (F /. i)) * (F /. i) by A10, RLVECT_2:def 7
.= (u . i) * (F /. i) by A5, A9 ;
:: thesis: verum

end;

hence ex g1, h1 being FinSequence of V ex a1 being INT -valued FinSequence st
( x = Sum h1 & rng g1 c= A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) ) by A6, A7, A8, A1, A2; :: thesis: verum