theorem :: FUNCOP_1:51

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