for A, D being set
for p being FinSequence of A
for f being Function of A,D holds f * p is FinSequence of D