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 4 :: thesis: o .: (f,f) = f

hence o .: (f,f) = f by A1, A3, FUNCT_1:2; :: thesis: verum

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 4 :: thesis: o .: (f,f) = f

A3: now :: thesis: for x being object st x in A holds

(o .: (f,f)) . x = f . x

dom f = A
by FUNCT_2:def 1;(o .: (f,f)) . x = f . x

let x be object ; :: 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:5;

thus (o .: (f,f)) . x = o . (a,a) by A1, A4, FUNCOP_1:22

.= f . x by A2 ; :: thesis: verum

end;assume A4: x in A ; :: thesis: (o .: (f,f)) . x = f . x

then reconsider a = f . x as Element of D by FUNCT_2:5;

thus (o .: (f,f)) . x = o . (a,a) by A1, A4, FUNCOP_1:22

.= f . x by A2 ; :: thesis: verum

hence o .: (f,f) = f by A1, A3, FUNCT_1:2; :: thesis: verum