let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; :: thesis: the addF of K is having_an_inverseOp
comp K is_an_inverseOp_wrt the addF of K by Th13;
hence the addF of K is having_an_inverseOp by FINSEQOP:def 2; :: thesis: verum