theorem :: FUNCOP_1:68

for X, Y being non empty set
for F being BinOp of X
for f being Function of Y,X
for y being Element of Y st F is idempotent holds
(F [:] (f,(f . y))) . y = f . y