:: deftheorem defines is_right_distributive_wrt BINOP_1:def 10 :
for A being set
for o9, o being BinOp of A holds
( o9 is_right_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) );