let i be Nat; :: 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 Th39
.= R by BINOP_2:2, FINSEQOP:57 ; :: thesis: verum