theorem :: FINSOP_1:11

for D being non empty set
for d being Element of D
for g being BinOp of D holds g "**" <*d*> = d by Lm4;