theorem Th2: :: FVSUM_1:2

for K being non empty add-associative addLoopStr holds the addF of K is associative