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

I is_continuous_in x0

let I be Function of REAL,(REAL-NS 1); :: thesis: ( I = (proj (1,1)) " implies I is_continuous_in x0 )

assume A1: I = (proj (1,1)) " ; :: thesis: I is_continuous_in x0

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;

I is_continuous_in x0

let I be Function of REAL,(REAL-NS 1); :: thesis: ( I = (proj (1,1)) " implies I is_continuous_in x0 )

assume A1: I = (proj (1,1)) " ; :: thesis: I is_continuous_in x0

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 ) )

hence
I is_continuous_in x0
by A3, NFCONT_3:8; :: thesis: verumex 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

end;( 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 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: verum

end;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 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: verum