reconsider n = n as Element of NAT by ORDINAL1:def 13;
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