let D be non empty set ; 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; for g being BinOp of D st len F = 2 holds
g "**" F = g . ((F . 1),(F . 2))
let g be BinOp of D; ( len F = 2 implies g "**" F = g . ((F . 1),(F . 2)) )
assume A1:
len F = 2
; 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
;
verum