let i be Nat; :: thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2)
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2)
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: - (R1 + R2) = (- R1) + (- R2)
(R1 + R2) + ((- R1) + (- R2)) = ((R1 + R2) + (- R1)) + (- R2) by FINSEQOP:28
.= ((R2 + R1) + (- R1)) + (- R2) by FINSEQOP:33
.= (R2 + (R1 + (- R1))) + (- R2) by FINSEQOP:28
.= (R2 + (i |-> (0. K))) + (- R2) by Lm3
.= R2 + (- R2) by Lm2
.= i |-> (0. K) by Lm3 ;
hence - (R1 + R2) = (- R1) + (- R2) by Th27; :: thesis: verum