reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider R1 = x, R2 = y as Element of n -tuples_on REAL ;
R1 + R2 in n -tuples_on REAL ;
hence x + y is Element of REAL n ; :: thesis: verum