theorem Th2: :: PRVECT_1:2

for G being AbGroup holds comp G is_an_inverseOp_wrt the addF of G