theorem :: FINSOP_1:9

for D being non empty set
for F, G, H being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Nat st k in dom F holds
F . k = g . ((G . k),(H . k)) ) holds
g "**" F = g . ((g "**" G),(g "**" H))