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