let n be non zero Element of NAT ; :: thesis: for Z being open Subset of REAL

for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) )

let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) )

let f be PartFunc of REAL,(REAL n); :: thesis: ( Z c= dom f & ex r being Element of REAL n st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) ) )

assume A1: Z c= dom f ; :: thesis: ( for r being Element of REAL n holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) ) )

given r being Element of REAL n such that A2: rng f = {r} ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) )

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

A3: r is Point of (REAL-NS n) by REAL_NS1:def 4;

then A4: ( g is_differentiable_on Z & ( for x being Real st x in Z holds

(g `| Z) /. x = 0. (REAL-NS n) ) ) by A1, A2, NDIFF_3:12;

(f `| Z) /. x = 0* n ) ) by A5, A1; :: thesis: verum

for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) )

let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n) st Z c= dom f & ex r being Element of REAL n st rng f = {r} holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) )

let f be PartFunc of REAL,(REAL n); :: thesis: ( Z c= dom f & ex r being Element of REAL n st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) ) )

assume A1: Z c= dom f ; :: thesis: ( for r being Element of REAL n holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) ) )

given r being Element of REAL n such that A2: rng f = {r} ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) /. x = 0* n ) )

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

A3: r is Point of (REAL-NS n) by REAL_NS1:def 4;

then A4: ( g is_differentiable_on Z & ( for x being Real st x in Z holds

(g `| Z) /. x = 0. (REAL-NS n) ) ) by A1, A2, NDIFF_3:12;

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

f | Z is_differentiable_in x

then A6:
f is_differentiable_on Z
by A1;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 A4, 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 A4, NDIFF_3:def 5;

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

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

(f `| Z) /. x = 0* n

hence
( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) /. x = 0* n

let x be Real; :: thesis: ( x in Z implies (f `| Z) /. x = 0* n )

assume A7: x in Z ; :: thesis: (f `| Z) /. x = 0* n

then A8: (g `| Z) /. x = 0. (REAL-NS n) by A3, A1, A2, NDIFF_3:12;

x in dom (g `| Z) by A4, A7, NDIFF_3:def 6;

then A9: (g `| Z) . x = 0. (REAL-NS n) by A8, PARTFUN1:def 6;

A10: (g `| Z) . x = diff (g,x) by A7, A4, NDIFF_3:def 6;

A11: (f `| Z) . x = diff (f,x) by A7, A6, Def4;

diff (f,x) = diff (g,x) by Th3;

then A12: (f `| Z) . x = 0* n by A9, A10, A11, REAL_NS1:def 4;

x in dom (f `| Z) by A6, Def4, A7;

hence (f `| Z) /. x = 0* n by A12, PARTFUN1:def 6; :: thesis: verum

end;assume A7: x in Z ; :: thesis: (f `| Z) /. x = 0* n

then A8: (g `| Z) /. x = 0. (REAL-NS n) by A3, A1, A2, NDIFF_3:12;

x in dom (g `| Z) by A4, A7, NDIFF_3:def 6;

then A9: (g `| Z) . x = 0. (REAL-NS n) by A8, PARTFUN1:def 6;

A10: (g `| Z) . x = diff (g,x) by A7, A4, NDIFF_3:def 6;

A11: (f `| Z) . x = diff (f,x) by A7, A6, Def4;

diff (f,x) = diff (g,x) by Th3;

then A12: (f `| Z) . x = 0* n by A9, A10, A11, REAL_NS1:def 4;

x in dom (f `| Z) by A6, Def4, A7;

hence (f `| Z) /. x = 0* n by A12, PARTFUN1:def 6; :: thesis: verum

(f `| Z) /. x = 0* n ) ) by A5, A1; :: thesis: verum