for n, i being Element of NAT
for x0 being Element of REAL n st 1 <= i & i <= n holds
proj (i,n) is_continuous_in x0