theorem Th13: :: FVSUM_1:13

for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds comp K is_an_inverseOp_wrt the addF of K