theorem Th16: :: FINSOP_1:16

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