let i be Element of NAT ; :: thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; :: thesis: for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2
let R1, R, R2 be Element of i -tuples_on the carrier of K; :: thesis: ( R1 + R = R2 + R implies R1 = R2 )
assume R1 + R = R2 + R ; :: thesis: R1 = R2
then R1 + (R + (- R)) = (R2 + R) + (- R) by FINSEQOP:29;
then ( R1 + (R + (- R)) = R2 + (R + (- R)) & R + (- R) = i |-> (0. K) ) by Lm3, FINSEQOP:29;
then R1 = R2 + (i |-> (0. K)) by Lm2;
hence R1 = R2 by Lm2; :: thesis: verum