let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for x being Element of G holds Double (- x) = - (Double x)
let x be Element of G; :: thesis: Double (- x) = - (Double x)
0. G = Double (0. G) by RLVECT_1:def 4
.= Double (x + (- x)) by RLVECT_1:def 10
.= (Double x) + (Double (- x)) by Th10 ;
hence Double (- x) = - (Double x) by RLVECT_1:6; :: thesis: verum