for D being non empty set
for b being BinOp of D
for d being Element of D holds b "**" <%d%> = d