let n be non zero Element of NAT ; for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
let Z be open Subset of REAL; for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
let f be PartFunc of REAL,(REAL n); for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
let r, p be Element of REAL n; ( Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + p ) implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) ) )
assume that
A1:
Z c= dom f
and
A2:
for x being Real st x in Z holds
f /. x = (x * r) + p
; ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
reconsider r1 = r, p1 = p as Point of (REAL-NS n) by REAL_NS1:def 4;
then A6:
( g is_differentiable_on Z & ( for x being Real st x in Z holds
(g `| Z) . x = r1 ) )
by A1, NDIFF_3:21;
hence A7:
f is_differentiable_on Z
by A1; for x being Real st x in Z holds
(f `| Z) . x = r
let x be Real; ( x in Z implies (f `| Z) . x = r )
assume A8:
x in Z
; (f `| Z) . x = r
then A9:
(g `| Z) . x = diff (g,x)
by A6, NDIFF_3:def 6;
A10:
(f `| Z) . x = diff (f,x)
by A8, A7, Def4;
diff (f,x) = diff (g,x)
by Th3;
hence
(f `| Z) . x = r
by A8, A3, A1, A9, A10, NDIFF_3:21; verum