let D be non empty set ; :: thesis: for F being FinSequence of D
for g being BinOp of D st len F = 2 holds
g "**" F = g . ((F . 1),(F . 2))
let F be FinSequence of D; :: thesis: for g being BinOp of D st len F = 2 holds
g "**" F = g . ((F . 1),(F . 2))
let g be BinOp of D; :: thesis: ( len F = 2 implies g "**" F = g . ((F . 1),(F . 2)) )
assume A1: len F = 2 ; :: thesis: g "**" F = g . ((F . 1),(F . 2))
then F = <*(F . 1),(F . 2)*> by FINSEQ_1:44
.= <*(F /. 1),(F . 2)*> by A1, FINSEQ_4:15
.= <*(F /. 1),(F /. 2)*> by A1, FINSEQ_4:15 ;
hence g "**" F = g . ((F /. 1),(F /. 2)) by Th12
.= g . ((F . 1),(F /. 2)) by A1, FINSEQ_4:15
.= g . ((F . 1),(F . 2)) by A1, FINSEQ_4:15 ;
:: thesis: verum