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;
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 ) )
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
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;
end;
hence J is_continuous_in x0 by A2, NFCONT_1:8; :: thesis: verum