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
f1 is_differentiable_on 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
f1 is_differentiable_on Z
let f1 be PartFunc of REAL,REAL; :: thesis: ( n >= 1 & f1 is_differentiable_on n,Z implies f1 is_differentiable_on Z )
assume that
A1: n >= 1 and
A2: f1 is_differentiable_on n,Z ; :: thesis: f1 is_differentiable_on Z
1 - 1 <= n - 1 by A1, XREAL_1:9;
then (diff (f1,Z)) . 0 is_differentiable_on Z by A2, TAYLOR_1:def 6;
then f1 | Z is_differentiable_on Z by TAYLOR_1:def 5;
hence f1 is_differentiable_on Z by Th6; :: thesis: verum