:: deftheorem defines * LANG1:def 13 :
for X, Y being non empty set
for f being Function of X,Y
for b₄ being Function of (X *),(Y *) holds
( b₄ = f * iff for p being Element of X * holds b₄ . p = f * p );