for Y, Z being set
for D being non empty set
for p being FinSequence
for f being Function of Y,D
for g being Function of Z,D st rng p c= Y & rng p c= Z & ( for a being object st a in rng p holds
f . a = g . a ) holds
f * p = g * p