let i be natural Number ; :: 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) by Th8, Th9, BINOP_2:2, FINSEQOP:74;
hence R1 = R2 ; :: thesis: verum