let n, i be Element of NAT ; :: thesis: for x0 being Element of REAL n st 1 <= i & i <= n holds
proj (i,n) is_continuous_in x0
let x0 be Element of REAL n; :: thesis: ( 1 <= i & i <= n implies proj (i,n) is_continuous_in x0 )
assume A1: ( 1 <= i & i <= n ) ; :: thesis: proj (i,n) is_continuous_in x0
A2: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
reconsider prg = proj (i,n) as PartFunc of (REAL-NS n),REAL by REAL_NS1:def 4;
reconsider px0 = x0 as Element of (REAL-NS n) by REAL_NS1:def 4;

now :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) )

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) ) )
assume A3: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) )
take s = r; :: thesis: ( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) )
thus 0 < s by A3; :: thesis: for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r

now :: thesis: for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < r holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r

let px1 be Element of (REAL-NS n); :: thesis: ( px1 in dom prg & ||.(px1 - px0).|| < r implies |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r )
assume A4: ( px1 in dom prg & ||.(px1 - px0).|| < r ) ; :: thesis: |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r
reconsider x1 = px1 as Element of REAL n by REAL_NS1:def 4;
A5: ||.(px1 - px0).|| = |.(x1 - x0).| by REAL_NS1:1, REAL_NS1:5;
(proj (i,n)) /. (x1 - x0) = ((proj (i,n)) /. x1) - ((proj (i,n)) /. x0) by A1, PDIFF_8:12;
then |.(((proj (i,n)) /. x1) - ((proj (i,n)) /. x0)).| <= |.(x1 - x0).| by A1, PDIFF_8:5;
hence |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r by A4, A5, XXREAL_0:2; :: thesis: verum

end;

hence for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds
|.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ; :: thesis: verum

end;

then prg is_continuous_in px0 by A2, NFCONT_1:8;
hence proj (i,n) is_continuous_in x0 ; :: thesis: verum