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 A1: f is_differentiable_on Z ; :: thesis: (f `| Z) `| Z = (diff f,Z) . 2
(f `| Z) `| Z = ((f | Z) `| Z) `| Z by A1, 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