let i be Nat; :: thesis: for R1, R2 being Element of i -tuples_on REAL st R1 - R2 = i |-> 0 holds
R1 = R2
let R1, R2 be Element of i -tuples_on REAL ; :: thesis: ( R1 - R2 = i |-> 0 implies R1 = R2 )
assume R1 - R2 = i |-> 0 ; :: thesis: R1 = R2
then R1 + (- R2) = i |-> 0 by FINSEQOP:89;
then R1 = - (- R2) by Th22, Th23, BINOP_2:2, FINSEQOP:78;
hence R1 = R2 ; :: thesis: verum