theorem :: FINSOP_1:17

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