theorem Th14: :: FVSUM_1:14

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