theorem :: FUNCOP_1:56

for X being non empty set
for F being BinOp of X
for x being Element of X holds (F [;] (x,(id X))) . x = F . (x,x)