let G be Group; :: thesis: ( G is commutative Group iff the multF of G is commutative )
thus ( G is commutative Group implies the multF of G is commutative ) :: thesis: ( the multF of G is commutative implies G is commutative Group )

proof

assume A1: G is commutative Group ; :: 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
thus the multF of G . a,b = a * b
.= b * a by A1, Lm1
.= the multF of G . b,a ; :: thesis: verum

end;

assume A2: the multF of G is commutative ; :: thesis: G is commutative Group
G is commutative

proof

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, BINOP_1:def 2; :: thesis: verum

end;

hence G is commutative Group ; :: thesis: verum