:: deftheorem defines is_distributive_wrt BINOP_1:def 20 :
for A being non empty set
for u being UnOp of A
for o being BinOp of A holds
( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );