for G being addGroup holds
( G is Abelian addGroup iff the addF of G is commutative )