:: deftheorem defines is_left_distributive_wrt BINOP_1:def 9 :
for A being set
for o9, o being BinOp of A holds
( o9 is_left_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))) );