let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; :: thesis: the_inverseOp_wrt the addF of K = comp K
A1: comp K is_an_inverseOp_wrt the addF of K by Th13;
( the addF of K is having_a_unity & the addF of K is having_an_inverseOp ) by Th8, Th14;
hence the_inverseOp_wrt the addF of K = comp K by A1, FINSEQOP:def 3; :: thesis: verum