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 15 :: thesis: (o,D .: A) . f,f = f
thus (o,D .: A) . f,f = o .: f,f by Def2
.= f by A1, Th7 ; :: thesis: verum