theorem Th34: :: MATRIX_0:34

for i being Nat
for D being non empty set
for M being FinSequence of D * holds M . i is FinSequence of D