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

proof

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

end;

assume A2: for a, b being Element of G holds a * b = b * a ; :: thesis: G is commutative
let a be Element of G; :: according to BINOP_1:def 13,MONOID_0:def 11 :: thesis: for b₁ being Element of the carrier of G holds the multF of G . (a,b₁) = the multF of G . (b₁,a)
let b be Element of G; :: thesis: the multF of G . (a,b) = the multF of G . (b,a)
( H₂(G) . (a,b) = a * b & H₂(G) . (b,a) = b * a ) ;
hence the multF of G . (a,b) = the multF of G . (b,a) by A2; :: thesis: verum