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

let i be Element of 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 <= n by A2, WSIERP_1:23;
(diff f,Z) . i is_differentiable_on Z by A2, A1, TAYLOR_1:def 6;
then r (#) ((diff f,Z) . i) is_differentiable_on Z by FDIFF_2:19;
hence (diff (r (#) f),Z) . i is_differentiable_on Z by Th13, a3, A1, TAYLOR_1:23; :: thesis: verum

end;

hence r (#) f is_differentiable_on n,Z by TAYLOR_1:def 6; :: thesis: verum