let f be PartFunc of REAL,REAL; for Z being Subset of REAL st Z c= dom f & Z is open & f is_differentiable_on 1,Z holds
( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z )
let Z be Subset of REAL; ( Z c= dom f & Z is open & f is_differentiable_on 1,Z implies ( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z ) )
assume AS:
( Z c= dom f & Z is open & f is_differentiable_on 1,Z )
; ( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z )
then
(diff (f,Z)) . 0 is_differentiable_on Z
;
then
f | Z is_differentiable_on Z
by TAYLOR_1:def 5;
hence X1:
f is_differentiable_on Z
by LM003, AS; (diff (f,Z)) . 1 = f `| Z
thus (diff (f,Z)) . 1 =
(diff (f,Z)) . (0 + 1)
.=
((diff (f,Z)) . 0) `| Z
by TAYLOR_1:def 5
.=
(f | Z) `| Z
by TAYLOR_1:def 5
.=
f `| Z
by AS, X1, LM00
; verum