let D be non empty set ; :: thesis: for d1, d2, d3 being Element of D
for g being BinOp of D holds g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3)
let d1, d2, d3 be Element of D; :: thesis: for g being BinOp of D holds g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3)
let g be BinOp of D; :: thesis: g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3)
A1: len <*d1,d2*> = 2 by FINSEQ_1:44;
thus g "**" <*d1,d2,d3*> = g "**" (<*d1,d2*> ^ <*d3*>) by FINSEQ_1:43
.= g . ((g "**" <*d1,d2*>),d3) by A1, Th4
.= g . ((g . (d1,d2)),d3) by Th12 ; :: thesis: verum