let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; :: thesis: comp K is_an_inverseOp_wrt the addF of K

now

let a be Element of K; :: thesis: ( the addF of K . a,((comp K) . a) = the_unity_wrt the addF of K & the addF of K . ((comp K) . a),a = the_unity_wrt the addF of K )
thus the addF of K . a,((comp K) . a) = a + (- a) by VECTSP_1:def 25
.= 0. K by RLVECT_1:16
.= the_unity_wrt the addF of K by Th9 ; :: thesis: the addF of K . ((comp K) . a),a = the_unity_wrt the addF of K
thus the addF of K . ((comp K) . a),a = (- a) + a by VECTSP_1:def 25
.= 0. K by RLVECT_1:16
.= the_unity_wrt the addF of K by Th9 ; :: thesis: verum

end;

hence comp K is_an_inverseOp_wrt the addF of K by FINSEQOP:def 1; :: thesis: verum