let i be Nat; :: thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds
R1 = R2
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds
R1 = R2
let R, R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: ( ( R1 + R = R2 + R or R1 + R = R + R2 ) implies R1 = R2 )
( R1 + R = R2 + R iff R1 + R = R + R2 ) by FINSEQOP:33;
hence ( ( R1 + R = R2 + R or R1 + R = R + R2 ) implies R1 = R2 ) by Lm4; :: thesis: verum