let m be non zero Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1)
for x1, x0, v being Element of REAL m st <>* f = g holds
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = |.(((diff (g,x1)) . v) - ((diff (g,x0)) . v)).|
let f be PartFunc of (REAL m),REAL; :: thesis: for g being PartFunc of (REAL m),(REAL 1)
for x1, x0, v being Element of REAL m st <>* f = g holds
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = |.(((diff (g,x1)) . v) - ((diff (g,x0)) . v)).|
let g be PartFunc of (REAL m),(REAL 1); :: thesis: for x1, x0, v being Element of REAL m st <>* f = g holds
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = |.(((diff (g,x1)) . v) - ((diff (g,x0)) . v)).|
let x1, x0, v be Element of REAL m; :: thesis: ( <>* f = g implies |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = |.(((diff (g,x1)) . v) - ((diff (g,x0)) . v)).| )
assume A1: <>* f = g ; :: thesis: |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = |.(((diff (g,x1)) . v) - ((diff (g,x0)) . v)).|
set I = proj (1,1);
reconsider w0 = (diff (g,x0)) . v, w1 = (diff (g,x1)) . v as Point of (REAL-NS 1) by REAL_NS1:def 4;
( dom (diff (g,x1)) = REAL m & dom (diff (g,x0)) = REAL m ) by FUNCT_2:def 1;
then ( (diff (f,x0)) . v = (proj (1,1)) . w0 & (diff (f,x1)) . v = (proj (1,1)) . w1 ) by A1, FUNCT_1:13;
then ((diff (f,x1)) . v) - ((diff (f,x0)) . v) = (proj (1,1)) . (w1 - w0) by PDIFF_1:4;
then |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = ||.(w1 - w0).|| by PDIFF_1:4;
hence |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = |.(((diff (g,x1)) . v) - ((diff (g,x0)) . v)).| by REAL_NS1:1, REAL_NS1:5; :: thesis: verum