theorem Th39: :: AFINSQ_2:39

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