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 Th48

.= f . y by A1 ; :: thesis: verum

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 Th48

.= f . y by A1 ; :: thesis: verum