let i be Nat; :: thesis: for R being Element of i -tuples_on REAL holds R - R = i |-> 0
let R be Element of i -tuples_on REAL ; :: thesis: R - R = i |-> 0
thus R - R = R + (- R) by FINSEQOP:89
.= i |-> 0 by Th22, Th23, BINOP_2:2, FINSEQOP:77 ; :: thesis: verum