theorem Th15: :: FVSUM_1:15

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