reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider R = x as Element of n -tuples_on REAL ;
r * R in n -tuples_on REAL ;
hence r (#) x is Element of REAL n ; :: thesis: verum