let D be non empty set ; :: thesis: 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; :: thesis: for g being BinOp of D holds g "**" <*d1,d2*> = g . d1,d2
let g be BinOp of D; :: thesis: g "**" <*d1,d2*> = g . d1,d2
A1: ( len <*d1*> = 1 & len <*d2*> = 1 ) by FINSEQ_1:56;
thus g "**" <*d1,d2*> = g "**" (<*d1*> ^ <*d2*>) by FINSEQ_1:def 9
.= g . (g "**" <*d1*>),d2 by A1, Th5
.= g . d1,d2 by Lm4 ; :: thesis: verum