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 that
A1: n >= 1 and
A2: f1 is_differentiable_on n,Z ; :: thesis: (diff f1,Z) . 1 = f1 `| Z
A3: f1 is_differentiable_on Z by ThB19, A1, A2;
(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 A3, FDIFF_2:16 ;
hence (diff f1,Z) . 1 = f1 `| Z ; :: thesis: verum