let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st f is_differentiable_on Z holds
(diff f,Z) . 1 = f `| Z
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_on Z implies (diff f,Z) . 1 = f `| Z )
assume A1: f is_differentiable_on Z ; :: thesis: (diff f,Z) . 1 = f `| Z
then A2: dom (f `| Z) = Z by FDIFF_1:def 8;
A3: for x being Real st x in Z holds
((diff f,Z) . 1) . x = (f `| Z) . x

proof

let x be Real; :: thesis: ( x in Z implies ((diff f,Z) . 1) . x = (f `| Z) . x )
assume x in Z ; :: thesis: ((diff f,Z) . 1) . x = (f `| Z) . x
((diff f,Z) . 1) . x = ((diff f,Z) . (1 + 0 )) . x
.= (((diff f,Z) . 0 ) `| Z) . x by TAYLOR_1:def 5
.= ((f | Z) `| Z) . x by TAYLOR_1:def 5
.= (f `| Z) . x by A1, FDIFF_2:16 ;
hence ((diff f,Z) . 1) . x = (f `| Z) . x ; :: thesis: verum

end;

dom ((diff f,Z) . 1) = dom ((diff f,Z) . (1 + 0 ))
.= dom (((diff f,Z) . 0 ) `| Z) by TAYLOR_1:def 5
.= dom ((f | Z) `| Z) by TAYLOR_1:def 5
.= dom (f `| Z) by A1, FDIFF_2:16
.= Z by A1, FDIFF_1:def 8 ;
hence (diff f,Z) . 1 = f `| Z by A2, A3, PARTFUN1:34; :: thesis: verum