let D be non empty set ; for d1, d2 being Element of D
for g being BinOp of D holds g "**" <*d1,d2*> = g . (d1,d2)
let d1, d2 be Element of D; for g being BinOp of D holds g "**" <*d1,d2*> = g . (d1,d2)
let g be BinOp of D; g "**" <*d1,d2*> = g . (d1,d2)
A1:
len <*d1*> = 1
by FINSEQ_1:39;
thus g "**" <*d1,d2*> =
g "**" (<*d1*> ^ <*d2*>)
by FINSEQ_1:def 9
.=
g . ((g "**" <*d1*>),d2)
by A1, Th4
.=
g . (d1,d2)
by Lm4
; verum