theorem Th14: :: FINSOP_1:14

for D being non empty set
for d1, d2, d3 being Element of D
for g being BinOp of D holds g "**" <*d1,d2,d3*> = g . ((g . (d1,d2)),d3)