let F be non trivial RealNormSpace; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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. F ) )
let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of F 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. F ) )
let f be PartFunc of REAL, the carrier of F; :: 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. F ) ) )
set R = REAL --> (0. F);
A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13;

now

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )

now

let n be Nat; :: thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
A2: rng h c= dom (REAL --> (0. F)) by A1;
A3: n in NAT by ORDINAL1:def 12;
hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def 2
.= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by FUNCOP_1:7, RLVECT_1:10 ;
:: thesis: verum

end;

then ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def 18;
hence ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; :: thesis: verum

end;

then reconsider R = REAL --> (0. F) as REST of F by Def1;
set L = REAL --> (0. F);

now

let p be Real; :: thesis: (REAL --> (0. F)) . p = p * (0. F)
thus (REAL --> (0. F)) . p = 0. F by FUNCOP_1:7
.= p * (0. F) by RLVECT_1:10 ; :: thesis: verum

end;

then reconsider L = REAL --> (0. F) as LINEAR of F by Def2;
assume that
A4: Z c= dom f and
A5: f | Z is constant ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0. F ) )
consider r being Point of F such that
A6: for x being Real st x in Z /\ (dom f) holds
f . x = r by A5, PARTFUN2:57;

A7: now

let x be Real; :: thesis: ( x in Z /\ (dom f) implies f /. x = r )
assume A8: x in Z /\ (dom f) ; :: thesis: f /. x = r
then x in dom f by XBOOLE_0:def 4;
hence f /. x = f . x by PARTFUN1:def 6
.= r by A8, A6 ;
:: thesis: verum

end;

A9: now

let x0 be Real; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A10: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A11: N c= Z by RCOMP_1:18;
A12: N c= dom f by A4, A11, XBOOLE_1:1;
A13: x0 in Z /\ (dom f) by A4, A10, XBOOLE_0:def 4;
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

proof

let x be Real; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A14: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def 6
.= 0. F by FUNCOP_1:7 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by A11, A12, XBOOLE_0:def 4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A7
.= r - r by A7, A13
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7
.= (L . (x - x0)) + (R /. (x - x0)) by A14, RLVECT_1:4 ;
:: thesis: verum

end;

hence f is_differentiable_in x0 by A12, Def3; :: thesis: verum

end;

hence A15: f is_differentiable_on Z by A4, Th10; :: thesis: for x being Real st x in Z holds
(f `| Z) . x = 0. F
let x0 be Real; :: thesis: ( x0 in Z implies (f `| Z) . x0 = 0. F )
assume A16: x0 in Z ; :: thesis: (f `| Z) . x0 = 0. F
then consider N being Neighbourhood of x0 such that
A17: N c= Z by RCOMP_1:18;
A18: N c= dom f by A4, A17, XBOOLE_1:1;
A19: x0 in Z /\ (dom f) by A4, A16, XBOOLE_0:def 4;
A20: for x being Real st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

proof

let x be Real; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A21: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def 6
.= 0. F by FUNCOP_1:7 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by A17, A18, XBOOLE_0:def 4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A7
.= r - r by A7, A19
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7
.= (L . (x - x0)) + (R /. (x - x0)) by A21, RLVECT_1:4 ;
:: thesis: verum

end;

A22: f is_differentiable_in x0 by A9, A16;
thus (f `| Z) . x0 = diff (f,x0) by A15, A16, Def6
.= L . 1 by A22, A18, A20, Def4
.= 0. F by FUNCOP_1:7 ; :: thesis: verum