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