let x0 be Real; :: thesis: for I being Function of REAL,() st I = (proj (1,1)) " holds
I is_continuous_in x0

let I be Function of REAL,(); :: thesis: ( I = (proj (1,1)) " implies I is_continuous_in x0 )
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: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Real st y1 in dom I & |.(y1 - y0).| < s holds
||.((I /. y1) - (I /. y0)).|| < r ) )
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Real st y1 in dom I & |.(y1 - y0).| < s holds
||.((I /. y1) - (I /. y0)).|| < r ) ) )

assume A5: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Real st y1 in dom I & |.(y1 - y0).| < s holds
||.((I /. y1) - (I /. y0)).|| < r ) )

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

thus 0 < s by A5; :: thesis: for y1 being Real st y1 in dom I & |.(y1 - y0).| < s holds
||.((I /. y1) - (I /. y0)).|| < r

thus for y1 being Real st y1 in dom I & |.(y1 - y0).| < s holds
||.((I /. y1) - (I /. y0)).|| < r :: thesis: verum
proof
let y1 be Real; :: thesis: ( y1 in dom I & |.(y1 - y0).| < s implies ||.((I /. y1) - (I /. y0)).|| < r )
assume A6: ( y1 in dom I & |.(y1 - y0).| < s ) ; :: thesis: ||.((I /. y1) - (I /. y0)).|| < r
reconsider x1 = y1 as Element of REAL by XREAL_0:def 1;
A7: ( I . x1 = I /. y1 & I . x0 = I /. x0 ) by ;
then reconsider Ia = I . x1, Ib = I . x0 as VECTOR of () ;
Ia - Ib = I . (x1 - x0) by ;
hence ||.((I /. y1) - (I /. y0)).|| < r by ; :: thesis: verum
end;
end;
hence I is_continuous_in x0 by ; :: thesis: verum