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