let A be set ; :: thesis: for D being non empty set
for o being BinOp of D st o is idempotent holds
(o,D) .: A is idempotent
let D be non empty set ; :: thesis: for o being BinOp of D st o is idempotent holds
(o,D) .: A is idempotent
let o be BinOp of D; :: thesis: ( o is idempotent implies (o,D) .: A is idempotent )
assume A1: o is idempotent ; :: thesis: (o,D) .: A is idempotent
let f be Element of Funcs (A,D); :: according to BINOP_1:def 4 :: thesis: ((o,D) .: A) . (f,f) = f
thus ((o,D) .: A) . (f,f) = o .: (f,f) by Def2
.= f by A1, Th6 ; :: thesis: verum