let i be natural Number ; :: thesis: for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2)
let R1, R2 be Element of i -tuples_on REAL; :: thesis: Sum (R1 + R2) = (Sum R1) + (Sum R2)
i is Nat by TARSKI:1;
hence Sum (R1 + R2) = addreal . ((addreal $$ R1),(addreal $$ R2)) by SETWOP_2:35
.= (Sum R1) + (Sum R2) by BINOP_2:def 9 ;
:: thesis: verum