let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )
let f be PartFunc of REAL,REAL; :: thesis: ( Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) ) )
set R = cf;
A1: dom cf = REAL by FUNCOP_1:13;

now

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )

A2: now

let n be Nat; :: thesis: ((h ") (#) (cf /* h)) . n = 0
A3: rng h c= dom cf by A1;
A4: n in NAT by ORDINAL1:def 12;
hence ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8
.= ((h ") . n) * (cf . (h . n)) by A4, A3, FUNCT_2:108
.= ((h ") . n) * 0 by FUNCOP_1:7
.= 0 ;
:: thesis: verum

end;

then A5: (h ") (#) (cf /* h) is constant 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 A5, SEQ_4:25; :: thesis: verum

end;

then reconsider R = cf as REST by Def3;
reconsider L = id REAL as PartFunc of REAL,REAL ;
for p being Real holds L . p = 1 * p by FUNCT_1:18;
then reconsider L = L as LINEAR by Def4;
assume that
A6: Z c= dom f and
A7: f | Z = id Z ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )

A8: now

let x be Real; :: thesis: ( x in Z implies f . x = x )
assume A9: x in Z ; :: thesis: f . x = x
then (f | Z) . x = x by A7, FUNCT_1:18;
hence f . x = x by A9, FUNCT_1:49; :: thesis: verum

end;

A10: now

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: 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)) )
assume x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
hence (f . x) - (f . x0) = x - (f . x0) by A8, A12
.= x - x0 by A8, A11
.= (L . (x - x0)) + 0 by FUNCT_1:18
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
:: thesis: verum

end;

N c= dom f by A6, A12, XBOOLE_1:1;
hence f is_differentiable_in x0 by A13, Def5; :: thesis: verum

end;

hence A14: f is_differentiable_on Z by A6, Th16; :: thesis: for x being Real st x in Z holds
(f `| Z) . x = 1
let x0 be Real; :: thesis: ( x0 in Z implies (f `| Z) . x0 = 1 )
assume A15: x0 in Z ; :: thesis: (f `| Z) . x0 = 1
then consider N1 being Neighbourhood of x0 such that
A16: N1 c= Z by RCOMP_1:18;
A17: f is_differentiable_in x0 by A10, A15;
then ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) by Def5;
then consider N being Neighbourhood of x0 such that
A18: N c= dom f ;
consider N2 being Neighbourhood of x0 such that
A19: N2 c= N1 and
A20: N2 c= N by RCOMP_1:17;
A21: N2 c= dom f by A18, A20, XBOOLE_1:1;
A22: for x being Real st x in N2 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

proof

let x be Real; :: thesis: ( x in N2 implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume x in N2 ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then x in N1 by A19;
hence (f . x) - (f . x0) = x - (f . x0) by A8, A16
.= x - x0 by A8, A15
.= (L . (x - x0)) + 0 by FUNCT_1:18
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
:: thesis: verum

end;

thus (f `| Z) . x0 = diff (f,x0) by A14, A15, Def8
.= L . 1 by A17, A21, A22, Def6
.= 1 by FUNCT_1:18 ; :: thesis: verum