let X be non empty set ; :: thesis: for Y being set

for F being BinOp of X

for f being Function of Y,X st F is idempotent holds

F .: (f,f) = f

let Y be set ; :: thesis: for F being BinOp of X

for f being Function of Y,X st F is idempotent holds

F .: (f,f) = f

let F be BinOp of X; :: thesis: for f being Function of Y,X st F is idempotent holds

F .: (f,f) = f

let f be Function of Y,X; :: thesis: ( F is idempotent implies F .: (f,f) = f )

assume A1: F is idempotent ; :: thesis: F .: (f,f) = f

for F being BinOp of X

for f being Function of Y,X st F is idempotent holds

F .: (f,f) = f

let Y be set ; :: thesis: for F being BinOp of X

for f being Function of Y,X st F is idempotent holds

F .: (f,f) = f

let F be BinOp of X; :: thesis: for f being Function of Y,X st F is idempotent holds

F .: (f,f) = f

let f be Function of Y,X; :: thesis: ( F is idempotent implies F .: (f,f) = f )

assume A1: F is idempotent ; :: thesis: F .: (f,f) = f

per cases
( Y = {} or Y <> {} )
;

end;

suppose A3:
Y <> {}
; :: thesis: F .: (f,f) = f

end;

now :: thesis: for y being Element of Y holds f . y = F . ((f . y),(f . y))

hence
F .: (f,f) = f
by A3, Th38; :: thesis: verumlet y be Element of Y; :: thesis: f . y = F . ((f . y),(f . y))

reconsider x = f . y as Element of X by A3, FUNCT_2:5;

thus f . y = F . (x,x) by A1

.= F . ((f . y),(f . y)) ; :: thesis: verum

end;reconsider x = f . y as Element of X by A3, FUNCT_2:5;

thus f . y = F . (x,x) by A1

.= F . ((f . y),(f . y)) ; :: thesis: verum