:: deftheorem defines :-> FUNCOP_1:def 10 :
for o, m, r being object
for b₄ being Function of [:{o},{m}:],{r} holds
( b₄ = (o,m) :-> r iff verum );