for p being FinSequence
for f being Function of (dom p),(dom p) holds p * f is FinSequence