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 integer-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 integer-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 integer-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 integer-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
P1: ( x = Sum z & rng z c= INT ) ;
consider F being FinSequence of V such that
P3: ( F is one-to-one & rng F = Carrier z & Sum z = Sum (z (#) F) ) by RLVECT_2:def 10;
P4: ( 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 9;
defpred S₁[ Nat, set ] means $2 = z . (F /. $1);

P5: now

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:6;
hence ex x being Element of INT st S₁[k,x] by P1; :: thesis: verum

end;

consider u being FinSequence of INT such that
P6: ( 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(P5);
X1: rng F c= A by P3, RLVECT_2:def 8;
X2: len F = len (z (#) F) by RLVECT_2:def 9;
X3: len F = len u by P6, FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in Seg (len F) implies (z (#) F) /. i = (u . i) * (F /. i) )
assume X51: i in Seg (len F) ; :: thesis: (z (#) F) /. i = (u . i) * (F /. i)
then X52: i in dom (z (#) F) by P4, FINSEQ_1:def 3;
hence (z (#) F) /. i = (z (#) F) . i by PARTFUN1:def 8
.= (z . (F /. i)) * (F /. i) by X52, RLVECT_2:def 9
.= (u . i) * (F /. i) by P6, X51 ;
:: thesis: verum

end;

hence ex g1, h1 being FinSequence of V ex a1 being integer-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 X1, X2, X3, P1, P3; :: thesis: verum