theorem Th36: :: ZMATRLIN:31

for V1 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for d being FinSequence of INT.Ring st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1