let m, n be non zero Element of NAT ; for Z being set
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g & f is_differentiable_on Z holds
f `| Z = g `| Z
let Z be set ; for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g & f is_differentiable_on Z holds
f `| Z = g `| Z
let f be PartFunc of (REAL m),(REAL n); for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g & f is_differentiable_on Z holds
f `| Z = g `| Z
let g be PartFunc of (REAL-NS m),(REAL-NS n); ( f = g & f is_differentiable_on Z implies f `| Z = g `| Z )
assume A1:
( f = g & f is_differentiable_on Z )
; f `| Z = g `| Z
then A2:
g is_differentiable_on Z
by PDIFF_6:30;
then A3:
dom (g `| Z) = Z
by NDIFF_1:def 9;
A4:
Z c= dom f
by A1, PDIFF_6:def 4;
then A5:
dom (f `| Z) = Z
by Def1;
now for x0 being object st x0 in dom (f `| Z) holds
(f `| Z) . x0 = (g `| Z) . x0let x0 be
object ;
( x0 in dom (f `| Z) implies (f `| Z) . x0 = (g `| Z) . x0 )assume A6:
x0 in dom (f `| Z)
;
(f `| Z) . x0 = (g `| Z) . x0then reconsider x =
x0 as
Element of
REAL m ;
reconsider Z1 =
Z as
Subset of
(REAL-NS m) by A2, NDIFF_1:30;
reconsider z =
x as
Point of
(REAL-NS m) by REAL_NS1:def 4;
Z1 is
open
by A2, NDIFF_1:32;
then
f is_differentiable_in x
by A1, A5, A6, PDIFF_6:32;
then A7:
ex
g0 being
PartFunc of
(REAL-NS m),
(REAL-NS n) ex
y0 being
Point of
(REAL-NS m) st
(
f = g0 &
x = y0 &
diff (
f,
x)
= diff (
g0,
y0) )
by PDIFF_1:def 8;
thus (f `| Z) . x0 =
(f `| Z) /. x
by A6, PARTFUN1:def 6
.=
diff (
g,
z)
by A4, A5, A6, A7, A1, Def1
.=
(g `| Z) /. x
by A6, A5, A2, NDIFF_1:def 9
.=
(g `| Z) . x0
by A6, A5, A3, PARTFUN1:def 6
;
verum end;
hence
f `| Z = g `| Z
by A5, A3, FUNCT_1:2; verum