theorem Th7: :: FVSUM_1:7

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