let m, n be non zero 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)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x0, x1 being Element of REAL m
for y0, y1 being Point of (REAL-NS m) st x0 = y0 & x1 = y1 & x0 in X & x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
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)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x0, x1 being Element of REAL m
for y0, y1 being Point of (REAL-NS m) st x0 = y0 & x1 = y1 & x0 in X & x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
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)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x0, x1 being Element of REAL m
for y0, y1 being Point of (REAL-NS m) st x0 = y0 & x1 = y1 & x0 in X & x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
let X be Subset of (REAL m); :: thesis: for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x0, x1 being Element of REAL m
for y0, y1 being Point of (REAL-NS m) st x0 = y0 & x1 = y1 & x0 in X & x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
let Y be Subset of (REAL-NS m); :: thesis: for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x0, x1 being Element of REAL m
for y0, y1 being Point of (REAL-NS m) st x0 = y0 & x1 = y1 & x0 in X & x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
let i be Nat; :: thesis: ( 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i implies for x0, x1 being Element of REAL m
for y0, y1 being Point of (REAL-NS m) st x0 = y0 & x1 = y1 & x0 in X & x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| )
assume A1: ( 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i ) ; :: thesis: for x0, x1 being Element of REAL m
for y0, y1 being Point of (REAL-NS m) st x0 = y0 & x1 = y1 & x0 in X & x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
let x0, x1 be Element of REAL m; :: thesis: for y0, y1 being Point of (REAL-NS m) st x0 = y0 & x1 = y1 & x0 in X & x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
let y0, y1 be Point of (REAL-NS m); :: thesis: ( x0 = y0 & x1 = y1 & x0 in X & x1 in X implies |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| )
assume A2: ( x0 = y0 & x1 = y1 & x0 in X & x1 in X ) ; :: thesis: |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
<*jj*> is Element of REAL 1 by FINSEQ_2:98;
then reconsider Pt1 = <*jj*> as Point of (REAL-NS 1) by REAL_NS1:def 4;
( (f `partial| (X,i)) /. x1 = partdiff (f,x1,i) & (f `partial| (X,i)) /. x0 = partdiff (f,x0,i) ) by A2, A1, PDIFF_7:def 5;
then ( (f `partial| (X,i)) /. x1 = (partdiff (g,y1,i)) . Pt1 & (f `partial| (X,i)) /. x0 = (partdiff (g,y0,i)) . Pt1 ) by Th21, A1, A2;
then ((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0) = ((partdiff (g,y1,i)) . Pt1) - ((partdiff (g,y0,i)) . Pt1) by REAL_NS1:5;
then A3: ((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0) = ((partdiff (g,y1,i)) - (partdiff (g,y0,i))) . Pt1 by LOPBAN_1:40;
||.Pt1.|| = |.1.| by PDIFF_8:2;
then ||.Pt1.|| = 1 by ABSVALUE:def 1;
then A4: ||.(((partdiff (g,y1,i)) - (partdiff (g,y0,i))) . Pt1).|| = ||.((partdiff (g,y1,i)) - (partdiff (g,y0,i))).|| * 1 by Th20;
g is_partial_differentiable_on Y,i by A1, PDIFF_7:33;
then ( (g `partial| (Y,i)) /. y1 = partdiff (g,y1,i) & (g `partial| (Y,i)) /. y0 = partdiff (g,y0,i) ) by A1, A2, PDIFF_1:def 20;
hence |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| by A3, A4, REAL_NS1:1; :: thesis: verum