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