:: deftheorem Def11 defines /* FUNCT_2:def 11 :
for X, Z being set
for Y being non empty set
for f being Function of X,Y
for p being b₂ -valued Function st rng f c= dom p holds
p /* f = p * f;