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