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