let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL st Z c= dom f & Z is open & f is_differentiable_on 1,Z holds
( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z )
let Z be Subset of REAL; :: thesis: ( Z c= dom f & Z is open & f is_differentiable_on 1,Z implies ( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z ) )
assume AS: ( Z c= dom f & Z is open & f is_differentiable_on 1,Z ) ; :: thesis: ( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z )
then (diff (f,Z)) . 0 is_differentiable_on Z ;
then f | Z is_differentiable_on Z by TAYLOR_1:def 5;
hence X1: f is_differentiable_on Z by LM003, AS; :: thesis: (diff (f,Z)) . 1 = f `| Z
thus (diff (f,Z)) . 1 = (diff (f,Z)) . (0 + 1)
.= ((diff (f,Z)) . 0) `| Z by TAYLOR_1:def 5
.= (f | Z) `| Z by TAYLOR_1:def 5
.= f `| Z by AS, X1, LM00 ; :: thesis: verum