theorem Th65: :: HILB10_7:65

for D being non empty set
for A, M being BinOp of D
for F, G being non-empty non empty FinSequence of D * st M is commutative & M is associative holds
M $$ (([#] (dom (F ^ G))),(A "**" (F ^ G))) = M . ((M $$ (([#] (dom F)),(A "**" F))),(M $$ (([#] (dom G)),(A "**" G))))