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

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

suppose A2: Y = {} ; :: thesis: F .: (f,f) = f

hence F .: (f,f) = {}
.= f by A2 ;
:: thesis: verum

end;

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

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

let 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;

hence F .: (f,f) = f by A3, Th38; :: thesis: verum

end;

end;