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

J is_continuous_in x0

let x0 be Point of (REAL-NS 1); :: thesis: ( J = proj (1,1) implies J is_continuous_in x0 )

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

A2: dom J = the carrier of (REAL-NS 1) by FUNCT_2:def 1;

J is_continuous_in x0

let x0 be Point of (REAL-NS 1); :: thesis: ( J = proj (1,1) implies J is_continuous_in x0 )

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

A2: dom J = the carrier of (REAL-NS 1) 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 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r ) )

hence
J is_continuous_in x0
by A2, NFCONT_1:8; :: thesis: verumex s being Real st

( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r ) )

let r be Real; :: thesis: ( 0 < r implies ex s being Real st

( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r ) ) )

assume A3: 0 < r ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r ) )

take s = r; :: thesis: ( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r ) )

thus 0 < s by A3; :: thesis: for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r

thus for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r :: thesis: verum

end;( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r ) ) )

assume A3: 0 < r ; :: thesis: ex s being Real st

( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r ) )

take s = r; :: thesis: ( 0 < s & ( for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r ) )

thus 0 < s by A3; :: thesis: for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r

thus for x1 being Point of (REAL-NS 1) st x1 in dom J & ||.(x1 - x0).|| < s holds

|.((J /. x1) - (J /. x0)).| < r :: thesis: verum

proof

let x1 be Point of (REAL-NS 1); :: thesis: ( x1 in dom J & ||.(x1 - x0).|| < s implies |.((J /. x1) - (J /. x0)).| < r )

(J /. x1) - (J /. x0) = J . (x1 - x0) by A1, PDIFF_1:4;

hence ( x1 in dom J & ||.(x1 - x0).|| < s implies |.((J /. x1) - (J /. x0)).| < r ) by A1, PDIFF_1:4; :: thesis: verum

end;(J /. x1) - (J /. x0) = J . (x1 - x0) by A1, PDIFF_1:4;

hence ( x1 in dom J & ||.(x1 - x0).|| < s implies |.((J /. x1) - (J /. x0)).| < r ) by A1, PDIFF_1:4; :: thesis: verum