let m, n be non zero Nat; :: thesis:
let f be PartFunc of (REAL m),(REAL n); :: thesis:
let X be set ; :: thesis:
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) ;

assume f is_continuous_on X ; :: thesis:
then A1: g is_continuous_on X by Th37;
hence A2: X c= dom f by NFCONT_1:19; :: thesis:
thus for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) :: thesis:

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 A3: ( x0 in X & 0 < r ) ; :: thesis:
then consider s being Real such that
A4: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.((g /. y1) - (g /. y0)).|| < r ) ) by A1, NFCONT_1:19;
take s ; :: thesis:
thus 0 < s by A4; :: thesis:

let x1 be Element of REAL m; :: thesis:
assume A5: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis:
reconsider y1 = x1 as Point of (REAL-NS m) by REAL_NS1:def 4;
( y1 in X & ||.(y1 - y0).|| < s ) by A5, REAL_NS1:1, REAL_NS1:5;
then A6: ||.((g /. y1) - (g /. y0)).|| < r by A4;
( g /. y1 = f /. x1 & g /. y0 = f /. x0 ) by A5, A2, A3, Th30;
hence |.((f /. x1) - (f /. x0)).| < r by A6, REAL_NS1:1, REAL_NS1:5; :: thesis:

end;

assume A7: ( X c= dom f & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) ; :: thesis:
for y0 being Point of (REAL-NS m)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.((g /. y1) - (g /. y0)).|| < r ) )

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 A8: ( y0 in X & 0 < r ) ; :: thesis:
then consider s being Real such that
A9: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) by A7;
take s ; :: thesis:
thus 0 < s by A9; :: thesis:

let y1 be Point of (REAL-NS m); :: thesis:
assume A10: ( y1 in X & ||.(y1 - y0).|| < s ) ; :: thesis:
reconsider x1 = y1 as Element of REAL m by REAL_NS1:def 4;
( x1 in X & |.(x1 - x0).| < s ) by A10, REAL_NS1:1, REAL_NS1:5;
then A11: |.((f /. x1) - (f /. x0)).| < r by A9;
( g /. y1 = f /. x1 & g /. y0 = f /. x0 ) by A10, A7, A8, Th30;
hence ||.((g /. y1) - (g /. y0)).|| < r by A11, REAL_NS1:1, REAL_NS1:5; :: thesis:

end;