let i be natural Number ; :: thesis: for R, R1 being Element of i -tuples_on REAL holds R1 = (R1 - R) + R
let R, R1 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 Th8, Th9, BINOP_2:2, FINSEQOP:73
.= (R1 - R) + R by FINSEQOP:28 ; :: thesis: verum