let n, i be Element of NAT ; :: thesis: for x0 being Point of (REAL-NS n) st 1 <= i & i <= n holds
Proj (i,n) is_continuous_in x0
let x0 be Point of (REAL-NS 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)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;

now :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) )

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

now :: thesis: for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r

let x1 be Point of (REAL-NS n); :: thesis: ( x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s implies ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r )
assume A4: ( x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s ) ; :: thesis: ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r
(Proj (i,n)) /. (x1 - x0) = ((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0) by A1, PDIFF_8:11;
then ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| <= ||.(x1 - x0).|| by A1, PDIFF_8:3;
hence ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r by A4, XXREAL_0:2; :: thesis: verum

end;

hence for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds
||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ; :: thesis: verum

end;

hence Proj (i,n) is_continuous_in x0 by A2, NFCONT_1:7; :: thesis: verum