let G be non empty multMagma ; :: thesis: ( G is idempotent iff for a being Element of G holds a * a = a )
thus ( G is idempotent implies for a being Element of G holds a * a = a ) :: thesis: ( ( for a being Element of G holds a * a = a ) implies G is idempotent )

proof

assume A1: for a being Element of G holds H₂(G) . (a,a) = a ; :: according to BINOP_1:def 4,MONOID_0:def 13 :: thesis: for a being Element of G holds a * a = a
let a be Element of G; :: thesis: a * a = a
thus a * a = a by A1; :: thesis: verum

end;

assume A2: for a being Element of G holds a * a = a ; :: thesis: G is idempotent
let a be Element of G; :: according to BINOP_1:def 4,MONOID_0:def 13 :: thesis: the multF of G . (a,a) = a
thus H₂(G) . (a,a) = a * a
.= a by A2 ; :: thesis: verum