let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st Z c= dom f & f | Z is V8() holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
let f be PartFunc of REAL,REAL; :: thesis: ( Z c= dom f & f | Z is V8() implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) ) )
reconsider cf = REAL --> (In (0,REAL)) as Function of REAL,REAL ;
set R = cf;
now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )
A2: now :: thesis: for n being Nat holds ((h ") (#) (cf /* h)) . n = 0
let n be Nat; :: thesis: ((h ") (#) (cf /* h)) . n = 0
A3: rng h c= dom cf ;
A5: n in NAT by ORDINAL1:def 12;
thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8
.= ((h ") . n) * (cf . (h . n)) by A5, A3, FUNCT_2:108
.= ((h ") . n) * 0
.= 0 ; :: thesis: verum
end;
then A6: (h ") (#) (cf /* h) is V8() by VALUED_0:def 18;
hence (h ") (#) (cf /* h) is convergent ; :: thesis: lim ((h ") (#) (cf /* h)) = 0
((h ") (#) (cf /* h)) . 0 = 0 by A2;
hence lim ((h ") (#) (cf /* h)) = 0 by A6, SEQ_4:25; :: thesis: verum
end;
then reconsider R = cf as RestFunc by Def2;
set L = cf;
for p being Real holds cf . p = 0 * p ;
then reconsider L = cf as LinearFunc by Def3;
assume that
A7: Z c= dom f and
A8: f | Z is V8() ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
consider r being Element of REAL such that
A9: for x being Element of REAL st x in Z /\ (dom f) holds
f . x = r by A8, PARTFUN2:57;
A10: now :: thesis: for x0 being Real st x0 in Z holds
f is_differentiable_in x0
let x0 be Real; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A11: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A12: N c= Z by RCOMP_1:18;
A13: N c= dom f by A7, A12;
A14: x0 in Z /\ (dom f) by A7, A11, 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)) )
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then x in Z /\ (dom f) by A12, A13, XBOOLE_0:def 4;
hence (f . x) - (f . x0) = r - (f . x0) by A9
.= r - r by A9, A14
.= (L . (xx - xx0)) + 0
.= (L . (x - x0)) + (R . (x - x0)) ;
:: thesis: verum
end;
hence f is_differentiable_in x0 by A13; :: thesis: verum
end;
hence A15: f is_differentiable_on Z by A7, Th9; :: thesis: for x being Real st x in Z holds
(f `| Z) . x = 0
let x0 be Real; :: thesis: ( x0 in Z implies (f `| Z) . x0 = 0 )
assume A16: x0 in Z ; :: thesis: (f `| Z) . x0 = 0
then consider N being Neighbourhood of x0 such that
A17: N c= Z by RCOMP_1:18;
A18: N c= dom f by A7, A17;
A19: x0 in Z /\ (dom f) by A7, 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)) )
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
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 A9
.= r - r by A9, A19
.= (L . (xx - xx0)) + 0
.= (L . (x - x0)) + (R . (x - x0)) ;
:: thesis: verum
end;
A21: f is_differentiable_in x0 by A10, A16;
reconsider j = 1 as Element of REAL by XREAL_0:def 1;
thus (f `| Z) . x0 = diff (f,x0) by A15, A16, Def7
.= L . j by A21, A18, A20, Def5
.= 0 ; :: thesis: verum