for n being Nat
for D being set
for e1 being FinSequence of D holds n |-> e1 is FinSequence of D *