let y0 be Point of (REAL-NS m); :: thesis:
let r be Real; :: thesis:
reconsider x0 = y0 as Element of REAL m by REAL_NS1:def 4;
assume ( y0 in Z & 0 < r ) ; :: thesis:
then consider s being Real such that
A4: ( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) by A2, A3, Th45;
take s = s; :: thesis:
thus 0 < s by A4; :: thesis:
let y1 be Point of (REAL-NS m); :: thesis:
assume A5: ( y1 in Z & ||.(y1 - y0).|| < s ) ; :: thesis:
reconsider x1 = y1 as Element of REAL m by REAL_NS1:def 4;
||.(y1 - y0).|| = |.(x1 - x0).| by REAL_NS1:1, REAL_NS1:5;
hence |.((g /. y1) - (g /. y0)).| < r by A1, A5, A4; :: thesis:

end;

end;

let x0 be Element of REAL m; :: thesis:
let r be Real; :: thesis:
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;
assume ( x0 in Z & 0 < r ) ; :: thesis:
then consider s being Real such that
A8: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Z & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) ) by A6, NFCONT_1:20;
take s = s; :: thesis:
thus 0 < s by A8; :: thesis:
let x1 be Element of REAL m; :: thesis:
assume A9: ( x1 in Z & |.(x1 - x0).| < s ) ; :: thesis:
reconsider y1 = x1 as Point of (REAL-NS m) by REAL_NS1:def 4;
||.(y1 - y0).|| = |.(x1 - x0).| by REAL_NS1:1, REAL_NS1:5;
hence |.((f /. x1) - (f /. x0)).| < r by A1, A9, A8; :: thesis:

end;