theorem :: SETWOP_2:30

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 associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
(G [;] (d,(id D))) . (F "**" p) = F "**" ((G [;] (d,(id D))) * p)