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 :: thesis: for a being Element of K holds
( 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 )

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 13
.= 0. K by RLVECT_1:5
.= the_unity_wrt the addF of K by Th7 ; :: 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 13
.= 0. K by RLVECT_1:5
.= the_unity_wrt the addF of K by Th7 ; :: thesis: verum

end;

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