let D be non empty set ; :: thesis: for A being BinOp of D
for f being FinSequence of D holds A "**" <*f*> = <*(A "**" f)*>
let A be BinOp of D; :: thesis: for f being FinSequence of D holds A "**" <*f*> = <*(A "**" f)*>
let f be FinSequence of D; :: thesis: A "**" <*f*> = <*(A "**" f)*>
A1: ( len (A "**" <*f*>) = len <*f*> & len <*f*> = 1 ) by CARD_1:def 7;
then ( 1 in dom <*f*> & <*f*> . 1 = f ) by FINSEQ_3:25;
then (A "**" <*f*>) . 1 = A "**" f by Def10;
hence A "**" <*f*> = <*(A "**" f)*> by FINSEQ_1:40, A1; :: thesis: verum