for D1, D2 being non empty set
for p being FinSequence of D1
for f being Function of D1,D2 holds
( dom (f * p) = dom p & len (f * p) = len p & ( for n being Nat st n in dom (f * p) holds
(f * p) . n = f . (p . n) ) )