let r be Real; 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 ; 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; 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; ( f is_differentiable_on n,Z implies r (#) f is_differentiable_on n,Z )
assume A1:
f is_differentiable_on n,Z
; r (#) f is_differentiable_on n,Z
now for i being Nat st i <= n - 1 holds
(diff ((r (#) f),Z)) . i is_differentiable_on Zlet i be
Nat;
( i <= n - 1 implies (diff ((r (#) f),Z)) . i is_differentiable_on Z )assume A2:
i <= n - 1
;
(diff ((r (#) f),Z)) . i is_differentiable_on ZA3:
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;
verum end;
hence
r (#) f is_differentiable_on n,Z
; verum