theorem Th35: :: RLVECT_X:35

for V being RealLinearSpace
for A being Subset of V
for x being set
for g1, h1 being FinSequence of V
for a1 being INT -valued FinSequence st x = Sum h1 & rng g1 c= Z_Lin 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) ) holds
x in Z_Lin A