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 )
assume A1: for a being Element of D holds o . a,a = a ; :: according to BINOP_1:def 15 :: thesis: o .: f,f = f
A2: ( dom f = A & dom (o .: f,f) = A ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in A implies (o .: f,f) . x = f . x )
assume A3: 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 A2, A3, FUNCOP_1:28
.= f . x by A1 ; :: thesis: verum

end;

hence o .: f,f = f by A2, FUNCT_1:9; :: thesis: verum