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 2,Z holds
( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z & f `| Z is_differentiable_on Z & (diff (f,Z)) . 2 = (f `| Z) `| Z )
let Z be Subset of REAL; :: thesis: ( Z c= dom f & Z is open & f is_differentiable_on 2,Z implies ( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z & f `| Z is_differentiable_on Z & (diff (f,Z)) . 2 = (f `| Z) `| Z ) )
assume AS: ( Z c= dom f & Z is open & f is_differentiable_on 2,Z ) ; :: thesis: ( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z & f `| Z is_differentiable_on Z & (diff (f,Z)) . 2 = (f `| Z) `| Z )
f is_differentiable_on 1,Z by AS, TAYLOR_1:23;
then A3: ( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z ) by AS, DIFF1;
(diff (f,Z)) . 2 = (diff (f,Z)) . (1 + 1)
.= (f `| Z) `| Z by TAYLOR_1:def 5, A3 ;
hence ( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z & f `| Z is_differentiable_on Z & (diff (f,Z)) . 2 = (f `| Z) `| Z ) by AS, A3; :: thesis: verum