theorem Th1: :: FVSUM_1:1

for K being non empty Abelian addLoopStr holds the addF of K is commutative