let i be natural Number ; :: thesis: for R being Element of i -tuples_on REAL holds R - (i |-> 0) = R
let R be Element of i -tuples_on REAL; :: thesis: R - (i |-> 0) = R
thus R - (i |-> 0) = R + (i |-> (- 0)) by Th21
.= R by BINOP_2:2, FINSEQOP:56 ; :: thesis: verum