let i be Nat; :: thesis: for K being non empty right_complementable Abelian 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
let K be non empty right_complementable Abelian 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
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: ( R1 - R2 = i |-> (0. K) implies R1 = R2 )
assume R1 - R2 = i |-> (0. K) ; :: thesis: R1 = R2
then R1 + (- R2) = i |-> (0. K) by FINSEQOP:84;
then R1 = - (- R2) by Th27;
hence R1 = R2 by Th28; :: thesis: verum