theorem :: SETWOP_2:40

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 . (d,(F "**" p)) = F "**" (G [;] (d,p))