theorem :: FUNCOP_1:44

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