theorem Th66: :: HILB10_7:66

for D being non empty set
for A, M being BinOp of D
for f being non empty FinSequence of D st M is commutative & M is associative holds
M $$ (([#] (dom <*f*>)),(A "**" <*f*>)) = A "**" f