theorem Th6: :: FINSOP_1:6

for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds
g "**" (<*d*> ^ F) = g . (d,(g "**" F))