for G being Group holds
( G is commutative Group iff the multF of G is commutative )