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