let X, Y be non empty set ; :: thesis: 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
let F be BinOp of X; :: thesis: 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
let f be Function of Y,X; :: thesis: for y being Element of Y st F is idempotent holds
(F [:] f,(f . y)) . y = f . y
let y be Element of Y; :: thesis: ( F is idempotent implies (F [:] f,(f . y)) . y = f . y )
assume A1: F is idempotent ; :: thesis: (F [:] f,(f . y)) . y = f . y
thus (F [:] f,(f . y)) . y = F . (f . y),(f . y) by Th60
.= f . y by A1, BINOP_1:def 4 ; :: thesis: verum