for n, i being Element of NAT
for x0 being Point of (REAL-NS n) st 1 <= i & i <= n holds
Proj (i,n) is_continuous_in x0