thus ( G is commutative implies the multF of G is commutative ) :: thesis: ( the multF of G is commutative implies G is commutative )

proof

assume A1: for a, b being Element of G holds a * b = b * a ; :: according to GROUP_1:def 16 :: thesis: the multF of G is commutative
let a be Element of G; :: according to BINOP_1:def 13 :: 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 A1; :: thesis: verum

end;

assume A2: for a, b being Element of G holds H₂(G) . a,b = H₂(G) . b,a ; :: according to BINOP_1:def 13 :: thesis: G is commutative
let a be Element of G; :: according to GROUP_1:def 16 :: thesis: for b₁ being Element of the carrier of G holds a [*] b₁ = b₁ [*] a
let b be Element of G; :: thesis: a [*] b = b [*] a
thus a [*] b = b [*] a by A2; :: thesis: verum