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