let m be non zero Element of NAT ; 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; 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); 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; ( <>* f = g implies |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = |.(((diff (g,x1)) . v) - ((diff (g,x0)) . v)).| )
assume A1:
<>* f = g
; |.(((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; verum