for D being non empty set
for d being Element of D
for g being BinOp of D holds g "**" (1 |-> d) = d