theorem Th8: :: FVSUM_1:8

for K being non empty left_zeroed right_zeroed addLoopStr holds the addF of K is having_a_unity