let D be non empty set ; :: thesis: 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
let A, M be BinOp of D; :: thesis: for f being non empty FinSequence of D st M is commutative & M is associative holds
M $$ (([#] (dom <*f*>)),(A "**" <*f*>)) = A "**" f
let f be non empty FinSequence of D; :: thesis: ( M is commutative & M is associative implies M $$ (([#] (dom <*f*>)),(A "**" <*f*>)) = A "**" f )
assume A1: ( M is commutative & M is associative ) ; :: thesis: M $$ (([#] (dom <*f*>)),(A "**" <*f*>)) = A "**" f
A2: ( dom <*f*> = Seg 1 & 1 in {1} ) by FINSEQ_1:38, TARSKI:def 1;
then reconsider O = 1 as Element of dom <*f*> by FINSEQ_1:2;
thus M $$ (([#] (dom <*f*>)),(A "**" <*f*>)) = (A "**" <*f*>) . O by A1, SETWISEO:17, A2, FINSEQ_1:2
.= <*(A "**" f)*> . O by Th62
.= A "**" f ; :: thesis: verum