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 Z: 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 S: Y <> {} ; :: thesis: F .: f,f = f

now

let y be Element of Y; :: thesis: f . y = F . (f . y),(f . y)
reconsider x = f . y as Element of X by S, FUNCT_2:7;
thus f . y = F . x,x by Z, BINOP_1:def 4
.= F . (f . y),(f . y) ; :: thesis: verum

end;

hence F .: f,f = f by S, Th49; :: thesis: verum

end;

end;