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 & f | Z is constant 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 & f | Z is constant 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 & f | Z is constant implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0* n ) ) )
assume that
A1: Z c= dom f and
A2: f | Z is constant ; :: 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: g | Z is constant by A2;
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, NDIFF_3:20;

now :: 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 A4, NDIFF_3:def 5;
hence f | Z is_differentiable_in x ; :: thesis: verum

end;

hence A5: f is_differentiable_on Z by A1; :: thesis: 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 A6: x in Z ; :: thesis: (f `| Z) . x = 0* n
then A7: (g `| Z) . x = 0. (REAL-NS n) by A3, A1, NDIFF_3:20;
A8: (g `| Z) . x = diff (g,x) by A6, A4, NDIFF_3:def 6;
A9: (f `| Z) . x = diff (f,x) by A6, A5, Def4;
diff (f,x) = diff (g,x) by Th3;
hence (f `| Z) . x = 0* n by A7, A8, A9, REAL_NS1:def 4; :: thesis: verum