theorem Th11: :: BINOP_1:11

for A being set
for o, o9 being BinOp of A holds
( o9 is_distributive_wrt o iff for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )