for C, D being non empty set
for B being Element of Fin C
for d, e being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (d,e) = e holds
G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))