theorem :: SETWOP_2:15

for C, D being non empty set
for B being Element of Fin C
for d 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 & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))