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
A: 1 - 1 <= n - 1 by A1, XREAL_1:11;
A3: (diff f1,Z) . 0 is_differentiable_on Z by A, A2, TAYLOR_1:def 6;
f1 | Z is_differentiable_on Z by A3, TAYLOR_1:def 5;
hence f1 is_differentiable_on Z by ThB1; :: thesis: verum