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 7;
A3: for x being Element of REAL st x in Z holds
((diff (f,Z)) . 1) . x = (f `| Z) . x
proof
let x be Element of 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 7 ;
hence (diff (f,Z)) . 1 = f `| Z by A2, A3, PARTFUN1:5; :: thesis: verum