let n be non zero Element of NAT ; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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;

(g `| Z) . x = r1 ) ) by A1, NDIFF_3:21;

(f `| Z) . x = r

let x be Real; :: thesis: ( x in Z implies (f `| Z) . x = r )

assume A8: x in Z ; :: thesis: (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; :: thesis: verum

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; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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;

A3: now :: thesis: for x being Real st x in Z holds

g /. x = (x * r1) + p1

then A6:
( g is_differentiable_on Z & ( for x being Real st x in Z holds g /. x = (x * r1) + p1

let x be Real; :: thesis: ( x in Z implies g /. x = (x * r1) + p1 )

assume x in Z ; :: thesis: g /. x = (x * r1) + p1

then A4: f /. x = (x * r) + p by A2;

A5: f /. x = g /. x by REAL_NS1:def 4;

x * r = x * r1 by REAL_NS1:3;

hence g /. x = (x * r1) + p1 by A4, A5, REAL_NS1:2; :: thesis: verum

end;assume x in Z ; :: thesis: g /. x = (x * r1) + p1

then A4: f /. x = (x * r) + p by A2;

A5: f /. x = g /. x by REAL_NS1:def 4;

x * r = x * r1 by REAL_NS1:3;

hence g /. x = (x * r1) + p1 by A4, A5, REAL_NS1:2; :: thesis: verum

(g `| Z) . x = r1 ) ) by A1, NDIFF_3:21;

now :: thesis: for x being Real st x in Z holds

f | Z is_differentiable_in x

hence A7:
f is_differentiable_on Z
by A1; :: thesis: for x being Real st x in Z holds f | Z is_differentiable_in x

let x be Real; :: thesis: ( x in Z implies f | Z is_differentiable_in x )

assume x in Z ; :: thesis: f | Z is_differentiable_in x

then g | Z is_differentiable_in x by A6, NDIFF_3:def 5;

hence f | Z is_differentiable_in x ; :: thesis: verum

end;assume x in Z ; :: thesis: f | Z is_differentiable_in x

then g | Z is_differentiable_in x by A6, NDIFF_3:def 5;

hence f | Z is_differentiable_in x ; :: thesis: verum

(f `| Z) . x = r

let x be Real; :: thesis: ( x in Z implies (f `| Z) . x = r )

assume A8: x in Z ; :: thesis: (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; :: thesis: verum