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