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

let x0 be Point of (); :: thesis: ( J = proj (1,1) implies J is_continuous_in x0 )
assume A1: J = proj (1,1) ; :: thesis:
A2: dom J = the carrier of () 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 () 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 () 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 () 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 () 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 () st x1 in dom J & ||.(x1 - x0).|| < s holds
|.((J /. x1) - (J /. x0)).| < r

thus for x1 being Point of () st x1 in dom J & ||.(x1 - x0).|| < s holds
|.((J /. x1) - (J /. x0)).| < r :: thesis: verum
proof
let x1 be Point of (); :: thesis: ( x1 in dom J & ||.(x1 - x0).|| < s implies |.((J /. x1) - (J /. x0)).| < r )
(J /. x1) - (J /. x0) = J . (x1 - x0) by ;
hence ( x1 in dom J & ||.(x1 - x0).|| < s implies |.((J /. x1) - (J /. x0)).| < r ) by ; :: thesis: verum
end;
end;
hence J is_continuous_in x0 by ; :: thesis: verum