let G be AbGroup; :: thesis: comp G is_an_inverseOp_wrt the addF of G

A1: 0. G is_a_unity_wrt the addF of G by Th1;

A1: 0. G is_a_unity_wrt the addF of G by Th1;

now :: thesis: for x being Element of G holds

( 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 )

hence
comp G is_an_inverseOp_wrt the addF of G
; :: thesis: verum( 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 )

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 13

.= 0. G by RLVECT_1:5

.= 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 13

.= 0. G by RLVECT_1:5

.= the_unity_wrt the addF of G by A1, BINOP_1:def 8 ; :: thesis: verum

end;thus the addF of G . (x,((comp G) . x)) = x + (- x) by VECTSP_1:def 13

.= 0. G by RLVECT_1:5

.= 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 13

.= 0. G by RLVECT_1:5

.= the_unity_wrt the addF of G by A1, BINOP_1:def 8 ; :: thesis: verum