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

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