let x0 be Real; :: thesis:
let I be Function of REAL,(REAL-NS 1); :: thesis:
assume A1: I = (proj (1,1)) " ; :: thesis:
A2: I is Function of REAL,(REAL 1) by REAL_NS1:def 4;
A3: dom I = REAL by FUNCT_2:def 1;
then A4: x0 in dom I by XREAL_0:def 1;
reconsider y0 = x0 as Element of REAL by XREAL_0:def 1;

now :: thesis:

let r be Real; :: thesis:
assume A5: 0 < r ; :: thesis:
reconsider s1 = r as Real ;
take s = s1; :: thesis:
thus 0 < s by A5; :: thesis:
thus for y1 being Real st y1 in dom I & |.(y1 - y0).| < s holds
||.((I /. y1) - (I /. y0)).|| < r :: thesis:

proof

let y1 be Real; :: thesis:
assume A6: ( y1 in dom I & |.(y1 - y0).| < s ) ; :: thesis:
reconsider x1 = y1 as Element of REAL by XREAL_0:def 1;
A7: ( I . x1 = I /. y1 & I . x0 = I /. x0 ) by A4, A6, PARTFUN1:def 6;
then reconsider Ia = I . x1, Ib = I . x0 as VECTOR of (REAL-NS 1) ;
Ia - Ib = I . (x1 - x0) by A1, A2, PDIFF_1:3;
hence ||.((I /. y1) - (I /. y0)).|| < r by A6, A1, A2, A7, PDIFF_1:3; :: thesis:

end;

end;

hence I is_continuous_in x0 by A3, NFCONT_3:8; :: thesis: