theorem Th12: :: ZMATRLIN:13

for V1 being free finite-rank Z_Module
for p2 being FinSequence of V1
for p1 being FinSequence of INT.Ring st dom p1 = dom p2 holds
dom (lmlt (p1,p2)) = dom p1