let r be Real; :: thesis: for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds
r (#) f is_differentiable_on n,Z
let n be Element of NAT ; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds
r (#) f is_differentiable_on n,Z
let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds
r (#) f is_differentiable_on n,Z
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_on n,Z implies r (#) f is_differentiable_on n,Z )
assume A1: f is_differentiable_on n,Z ; :: thesis: r (#) f is_differentiable_on n,Z
now :: thesis: for i being Nat st i <= n - 1 holds
(diff ((r (#) f),Z)) . i is_differentiable_on Z
let i be Nat; :: thesis: ( i <= n - 1 implies (diff ((r (#) f),Z)) . i is_differentiable_on Z )
assume A2: i <= n - 1 ; :: thesis: (diff ((r (#) f),Z)) . i is_differentiable_on Z
A3: i in NAT by ORDINAL1:def 12;
(diff (f,Z)) . i is_differentiable_on Z by A1, A2;
then A4: r (#) ((diff (f,Z)) . i) is_differentiable_on Z by FDIFF_2:19;
i <= n by A2, WSIERP_1:18;
hence (diff ((r (#) f),Z)) . i is_differentiable_on Z by A1, A4, Th21, TAYLOR_1:23, A3; :: thesis: verum
end;
hence r (#) f is_differentiable_on n,Z ; :: thesis: verum