let D be non empty set ; :: thesis: 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))))
let A, M be BinOp of D; :: thesis: 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))))
let F, G be non-empty non empty FinSequence of D * ; :: thesis: ( M is commutative & M is associative implies M $$ (([#] (dom (F ^ G))),(A "**" (F ^ G))) = M . ((M $$ (([#] (dom F)),(A "**" F))),(M $$ (([#] (dom G)),(A "**" G)))) )
A1: ( dom (A "**" (F ^ G)) = dom (F ^ G) & dom (A "**" F) = dom F & dom (A "**" G) = dom G ) by FUNCT_2:def 1;
A "**" (F ^ G) = (A "**" F) ^ (A "**" G) by Th63;
hence ( M is commutative & M is associative implies M $$ (([#] (dom (F ^ G))),(A "**" (F ^ G))) = M . ((M $$ (([#] (dom F)),(A "**" F))),(M $$ (([#] (dom G)),(A "**" G)))) ) by A1, Th64; :: thesis: verum