let n be Element of NAT ; :: thesis: for Z being open Subset of REAL
for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds
(diff (f1,Z)) . 1 = f1 `| Z
let Z be open Subset of REAL; :: thesis: for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds
(diff (f1,Z)) . 1 = f1 `| Z
let f1 be PartFunc of REAL,REAL; :: thesis: ( n >= 1 & f1 is_differentiable_on n,Z implies (diff (f1,Z)) . 1 = f1 `| Z )
assume ( n >= 1 & f1 is_differentiable_on n,Z ) ; :: thesis: (diff (f1,Z)) . 1 = f1 `| Z
then A1: f1 is_differentiable_on Z by Th7;
(diff (f1,Z)) . 1 = (diff (f1,Z)) . (1 + 0)
.= ((diff (f1,Z)) . 0) `| Z by TAYLOR_1:def 5
.= (f1 | Z) `| Z by TAYLOR_1:def 5
.= f1 `| Z by A1, FDIFF_2:16 ;
hence (diff (f1,Z)) . 1 = f1 `| Z ; :: thesis: verum