let A be set ; :: thesis: for D being non empty set
for o being BinOp of D
for f being Function of A,D st o is idempotent holds
o .: f,f = f
let D be non empty set ; :: thesis: for o being BinOp of D
for f being Function of A,D st o is idempotent holds
o .: f,f = f
let o be BinOp of D; :: thesis: for f being Function of A,D st o is idempotent holds
o .: f,f = f
let f be Function of A,D; :: thesis: ( o is idempotent implies o .: f,f = f )
A1: dom (o .: f,f) = A by FUNCT_2:def 1;
assume A2: for a being Element of D holds o . a,a = a ; :: according to BINOP_1:def 15 :: thesis: o .: f,f = f

A3: now

let x be set ; :: thesis: ( x in A implies (o .: f,f) . x = f . x )
assume A4: x in A ; :: thesis: (o .: f,f) . x = f . x
then reconsider a = f . x as Element of D by FUNCT_2:7;
thus (o .: f,f) . x = o . a,a by A1, A4, FUNCOP_1:28
.= f . x by A2 ; :: thesis: verum

end;

dom f = A by FUNCT_2:def 1;
hence o .: f,f = f by A1, A3, FUNCT_1:9; :: thesis: verum