theorem :: RLVECT_X:25

for V being RealLinearSpace
for A being Subset of V
for x being set holds
( x in Z_Lin A iff 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 Lm1, Lm2;