let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds
(f `| Z) `| Z = (diff (f,Z)) . 2
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_on Z implies (f `| Z) `| Z = (diff (f,Z)) . 2 )
assume f is_differentiable_on Z ; :: thesis: (f `| Z) `| Z = (diff (f,Z)) . 2
then (f `| Z) `| Z = ((f | Z) `| Z) `| Z by FDIFF_2:16
.= (((diff (f,Z)) . 0) `| Z) `| Z by TAYLOR_1:def 5
.= ((diff (f,Z)) . (0 + 1)) `| Z by TAYLOR_1:def 5
.= (diff (f,Z)) . (1 + 1) by TAYLOR_1:def 5 ;
hence (f `| Z) `| Z = (diff (f,Z)) . 2 ; :: thesis: verum