for i being natural Number
for R being Element of i -tuples_on REAL holds (i |-> 0) - R = - R by BINOP_2:2, FINSEQOP:56;