let m, n be non zero Element of NAT ; :: thesis:
let f be PartFunc of (REAL m),(REAL n); :: thesis:
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis:
let X be Subset of (REAL m); :: thesis:
let Y be Subset of (REAL-NS m); :: thesis:
assume A1: ( X is open & X c= dom f & g = f & X = Y ) ; :: thesis:

hereby :: thesis:

assume A2: ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) ; :: thesis:
hence A3: f is_differentiable_on X by A1, PDIFF_6:30; :: thesis:
let x0 be Element of REAL m; :: thesis:
let r be Real; :: thesis:
assume A4: ( x0 in X & 0 < r ) ; :: thesis:
reconsider xx0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;
consider s being Real such that
A5: ( 0 < s & ( for xx1 being Point of (REAL-NS m) st xx1 in Y & ||.(xx1 - xx0).|| < s holds
||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| < r ) ) by A1, A2, A4, NFCONT_1:19;
take s = s; :: thesis:
thus 0 < s by A5; :: thesis:
let x1 be Element of REAL m; :: thesis:
assume A6: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis:
reconsider xx1 = x1 as Point of (REAL-NS m) by REAL_NS1:def 4;
||.(xx1 - xx0).|| < s by A6, REAL_NS1:1, REAL_NS1:5;
then A7: ||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| < r by A5, A6, A1;
let v be Element of REAL m; :: thesis:
reconsider vv = v as Point of (REAL-NS m) by REAL_NS1:def 4;
f is_differentiable_in x0 by A4, A1, A3, PDIFF_6:32;
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x0 = y & diff (f,x0) = diff (g,y) ) by PDIFF_1:def 8;
then A8: ((g `| Y) /. xx0) . vv = (diff (f,x0)) . v by A1, A4, A2, NDIFF_1:def 9;
f is_differentiable_in x1 by A6, A1, A3, PDIFF_6:32;
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x1 = y & diff (f,x1) = diff (g,y) ) by PDIFF_1:def 8;
then A9: ((g `| Y) /. xx1) . vv = (diff (f,x1)) . v by A1, A6, A2, NDIFF_1:def 9;
reconsider g10 = ((g `| Y) /. xx1) - ((g `| Y) /. xx0) as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;
(((g `| Y) /. xx1) . vv) - (((g `| Y) /. xx0) . vv) = g10 . vv by LOPBAN_1:40;
then A10: ||.((((g `| Y) /. xx1) . vv) - (((g `| Y) /. xx0) . vv)).|| <= ||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| * ||.vv.|| by LOPBAN_1:32;
||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| * ||.vv.|| <= r * ||.vv.|| by A7, XREAL_1:64;
then ||.((((g `| Y) /. xx1) . vv) - (((g `| Y) /. xx0) . vv)).|| <= r * ||.vv.|| by A10, XXREAL_0:2;
then |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * ||.vv.|| by A9, A8, REAL_NS1:1, REAL_NS1:5;
hence |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| by REAL_NS1:1; :: thesis:

end;

assume A11: ( f is_differentiable_on X & ( 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
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) ; :: thesis:
hence A12: g is_differentiable_on Y by A1, PDIFF_6:30; :: thesis:
then A13: dom (g `| Y) = Y by NDIFF_1:def 9;
for x0 being Point of (REAL-NS m)
for r being Real st x0 in Y & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in Y & ||.(x1 - x0).|| < s holds
||.(((g `| Y) /. x1) - ((g `| Y) /. x0)).|| < r ) )

proof

let xx0 be Point of (REAL-NS m); :: thesis:
let r0 be Real; :: thesis:
assume A14: ( xx0 in Y & 0 < r0 ) ; :: thesis:
set r = r0 / 2;
A15: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A14, XREAL_1:216;
reconsider x0 = xx0 as Element of REAL m by REAL_NS1:def 4;
consider s being Real such that
A16: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= (r0 / 2) * |.v.| ) ) by A11, A1, A14;
take s ; :: thesis:
thus 0 < s by A16; :: thesis:
let xx1 be Point of (REAL-NS m); :: thesis:
assume A17: ( xx1 in Y & ||.(xx1 - xx0).|| < s ) ; :: thesis:
reconsider x1 = xx1 as Element of REAL m by REAL_NS1:def 4;
A18: |.(x1 - x0).| < s by A17, REAL_NS1:1, REAL_NS1:5;

now :: thesis:

let vv be Point of (REAL-NS m); :: thesis:
assume ||.vv.|| <= 1 ; :: thesis:
reconsider v = vv as Element of REAL m by REAL_NS1:def 4;
f is_differentiable_in x0 by A14, A1, A11, PDIFF_6:32;
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x0 = y & diff (f,x0) = diff (g,y) ) by PDIFF_1:def 8;
then A19: ((g `| Y) /. xx0) . vv = (diff (f,x0)) . v by A1, A12, A14, NDIFF_1:def 9;
f is_differentiable_in x1 by A17, A1, A11, PDIFF_6:32;
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x1 = y & diff (f,x1) = diff (g,y) ) by PDIFF_1:def 8;
then A20: ((g `| Y) /. xx1) . vv = (diff (f,x1)) . v by A1, A12, A17, NDIFF_1:def 9;
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= (r0 / 2) * |.v.| by A18, A16, A17, A1;
then |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= (r0 / 2) * ||.vv.|| by REAL_NS1:1;
then ||.((((g `| Y) /. xx1) . vv) - (((g `| Y) /. xx0) . vv)).|| <= (r0 / 2) * ||.vv.|| by A20, A19, REAL_NS1:1, REAL_NS1:5;
hence ||.((((g `| Y) /. xx1) - ((g `| Y) /. xx0)) . vv).|| <= (r0 / 2) * ||.vv.|| by LOPBAN_1:40; :: thesis:

end;

then ||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| <= r0 / 2 by A14, Th1;
hence ||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| < r0 by A15, XXREAL_0:2; :: thesis:

end;

hence g `| Y is_continuous_on Y by A13, NFCONT_1:19; :: thesis: