let i be Nat; :: thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds
( R1 = - R2 & R2 = - R1 )
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; :: thesis: for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds
( R1 = - R2 & R2 = - R1 )
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: ( R1 + R2 = i |-> (0. K) implies ( R1 = - R2 & R2 = - R1 ) )
A1: ( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15;
( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th7, Th8;
hence ( R1 + R2 = i |-> (0. K) implies ( R1 = - R2 & R2 = - R1 ) ) by A1, FINSEQOP:74; :: thesis: verum