let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: comp G is_an_inverseOp_wrt the addF of G
A1: 0. G is_a_unity_wrt the addF of G by Th3;

now

let x be Element of G; :: thesis: ( the addF of G . x,((comp G) . x) = the_unity_wrt the addF of G & the addF of G . ((comp G) . x),x = the_unity_wrt the addF of G )
thus the addF of G . x,((comp G) . x) = x + (- x) by VECTSP_1:def 25
.= 0. G by RLVECT_1:16
.= the_unity_wrt the addF of G by A1, BINOP_1:def 8 ; :: thesis: the addF of G . ((comp G) . x),x = the_unity_wrt the addF of G
thus the addF of G . ((comp G) . x),x = ((comp G) . x) + x
.= x + (- x) by VECTSP_1:def 25
.= 0. G by RLVECT_1:16
.= the_unity_wrt the addF of G by A1, BINOP_1:def 8 ; :: thesis: verum

end;

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