theorem :: SETWOP_2:41

for D being non empty set
for d being Element of D
for F, G being BinOp of D
for p being FinSequence of 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 "**" p),d) = F "**" (G [:] (p,d))