for B being AbGroup holds multMagma(# the carrier of B, the addF of B #) is commutative Group