let m, n be non empty Element of NAT ; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st X is open & X c= dom f & g = f & X = Y holds
( g is_differentiable_on Y & g `| Y is_continuous_on Y iff ( 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.| ) ) ) ) )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st X is open & X c= dom f & g = f & X = Y holds
( g is_differentiable_on Y & g `| Y is_continuous_on Y iff ( 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.| ) ) ) ) )
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st X is open & X c= dom f & g = f & X = Y holds
( g is_differentiable_on Y & g `| Y is_continuous_on Y iff ( 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.| ) ) ) ) )
let X be Subset of (REAL m); :: thesis: for Y being Subset of (REAL-NS m) st X is open & X c= dom f & g = f & X = Y holds
( g is_differentiable_on Y & g `| Y is_continuous_on Y iff ( 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.| ) ) ) ) )
let Y be Subset of (REAL-NS m); :: thesis: ( X is open & X c= dom f & g = f & X = Y implies ( g is_differentiable_on Y & g `| Y is_continuous_on Y iff ( 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.| ) ) ) ) ) )
assume AS: ( X is open & X c= dom f & g = f & X = Y ) ; :: thesis: ( g is_differentiable_on Y & g `| Y is_continuous_on Y iff ( 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.| ) ) ) ) )
then O1: Y is open by OPEN;

hereby :: thesis: ( 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.| ) ) ) implies ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) )

assume AS1: ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) ; :: thesis: ( 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.| ) ) ) )
hence Z1: f is_differentiable_on X by AS, PDIFF_6:30; :: thesis: 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.| ) )
let x0 be Element of REAL m; :: thesis: 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.| ) )
let r be Real; :: thesis: ( x0 in X & 0 < r implies 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.| ) ) )
assume P2: ( x0 in X & 0 < r ) ; :: thesis: 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.| ) )
reconsider xx0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;
consider s being Real such that
P3: ( 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 AS, AS1, P2, NFCONT_1:19;
take s = s; :: thesis: ( 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.| ) )
thus 0 < s by P3; :: thesis: 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.|
let x1 be Element of REAL m; :: thesis: ( x1 in X & |.(x1 - x0).| < s implies for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| )
assume P4: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis: for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|
reconsider xx1 = x1 as Point of (REAL-NS m) by REAL_NS1:def 4;
||.(xx1 - xx0).|| < s by P4, REAL_NS1:1, REAL_NS1:5;
then P5: ||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| < r by P3, P4, AS;
let v be Element of REAL m; :: thesis: |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|
reconsider vv = v as Point of (REAL-NS m) by REAL_NS1:def 4;
f is_differentiable_in x0 by P2, AS, Z1, O1, 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 P8: ((g `| Y) /. xx0) . vv = (diff (f,x0)) . v by AS, P2, AS1, NDIFF_1:def 9;
f is_differentiable_in x1 by P4, AS, Z1, O1, 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 P7: ((g `| Y) /. xx1) . vv = (diff (f,x1)) . v by AS, P4, AS1, 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 D2: ||.((((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 P5, XREAL_1:64;
then ||.((((g `| Y) /. xx1) . vv) - (((g `| Y) /. xx0) . vv)).|| <= r * ||.vv.|| by D2, XXREAL_0:2;
then |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * ||.vv.|| by P7, P8, REAL_NS1:1, REAL_NS1:5;
hence |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| by REAL_NS1:1; :: thesis: verum

end;

assume P1: ( 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: ( g is_differentiable_on Y & g `| Y is_continuous_on Y )
hence Z1: g is_differentiable_on Y by AS, PDIFF_6:30; :: thesis: g `| Y is_continuous_on Y
then Z2: 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: for r being Real st xx0 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 - xx0).|| < s holds
||.(((g `| Y) /. x1) - ((g `| Y) /. xx0)).|| < r ) )
let r0 be Real; :: thesis: ( xx0 in Y & 0 < r0 implies ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in Y & ||.(x1 - xx0).|| < s holds
||.(((g `| Y) /. x1) - ((g `| Y) /. xx0)).|| < r0 ) ) )
assume P2: ( xx0 in Y & 0 < r0 ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in Y & ||.(x1 - xx0).|| < s holds
||.(((g `| Y) /. x1) - ((g `| Y) /. xx0)).|| < r0 ) )
set r = r0 / 2;
P21: ( 0 < r0 / 2 & r0 / 2 < r0 ) by P2, XREAL_1:216;
reconsider x0 = xx0 as Element of REAL m by REAL_NS1:def 4;
consider s being Real such that
P3: ( 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 P1, AS, P2;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in Y & ||.(x1 - xx0).|| < s holds
||.(((g `| Y) /. x1) - ((g `| Y) /. xx0)).|| < r0 ) )
thus 0 < s by P3; :: thesis: for x1 being Point of (REAL-NS m) st x1 in Y & ||.(x1 - xx0).|| < s holds
||.(((g `| Y) /. x1) - ((g `| Y) /. xx0)).|| < r0
let xx1 be Point of (REAL-NS m); :: thesis: ( xx1 in Y & ||.(xx1 - xx0).|| < s implies ||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| < r0 )
assume P4: ( xx1 in Y & ||.(xx1 - xx0).|| < s ) ; :: thesis: ||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| < r0
reconsider x1 = xx1 as Element of REAL m by REAL_NS1:def 4;
P5: |.(x1 - x0).| < s by P4, REAL_NS1:1, REAL_NS1:5;

now :: thesis: for vv being Point of (REAL-NS m) st ||.vv.|| <= 1 holds
||.((((g `| Y) /. xx1) - ((g `| Y) /. xx0)) . vv).|| <= (r0 / 2) * ||.vv.||

let vv be Point of (REAL-NS m); :: thesis: ( ||.vv.|| <= 1 implies ||.((((g `| Y) /. xx1) - ((g `| Y) /. xx0)) . vv).|| <= (r0 / 2) * ||.vv.|| )
assume ||.vv.|| <= 1 ; :: thesis: ||.((((g `| Y) /. xx1) - ((g `| Y) /. xx0)) . vv).|| <= (r0 / 2) * ||.vv.||
reconsider v = vv as Element of REAL m by REAL_NS1:def 4;
f is_differentiable_in x0 by P2, AS, P1, O1, 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 P8: ((g `| Y) /. xx0) . vv = (diff (f,x0)) . v by AS, Z1, P2, NDIFF_1:def 9;
f is_differentiable_in x1 by P4, AS, P1, O1, 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 P7: ((g `| Y) /. xx1) . vv = (diff (f,x1)) . v by AS, Z1, P4, NDIFF_1:def 9;
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= (r0 / 2) * |.v.| by P5, P3, P4, AS;
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 P7, P8, REAL_NS1:1, REAL_NS1:5;
hence ||.((((g `| Y) /. xx1) - ((g `| Y) /. xx0)) . vv).|| <= (r0 / 2) * ||.vv.|| by LOPBAN_1:40; :: thesis: verum

end;

then ||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| <= r0 / 2 by P2, LM01CPre2;
hence ||.(((g `| Y) /. xx1) - ((g `| Y) /. xx0)).|| < r0 by P21, XXREAL_0:2; :: thesis: verum

end;

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