let i be Nat; :: thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds - (- R) = R
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; :: thesis: for R being Element of i -tuples_on the carrier of K holds - (- R) = R
let R be Element of i -tuples_on the carrier of K; :: thesis: - (- R) = R
R + (- R) = i |-> (0. K) by Lm3;
hence - (- R) = R by Th27; :: thesis: verum