theorem :: VECTSP_1:35

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