theorem Th6: :: FVSUM_1:6

for K being non empty left_zeroed right_zeroed addLoopStr holds 0. K is_a_unity_wrt the addF of K