theorem Th36: :: MATRLIN:36

for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for d being FinSequence of K st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1