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
A3: now :: thesis: for x being object st x in A holds
(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;
dom f = A by FUNCT_2:def 1;
hence o .: (f,f) = f by A1, A3, FUNCT_1:2; :: thesis: verum