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
(diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n)
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
(diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n)
let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds
(diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n)
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_on n,Z implies (diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n) )
defpred S₁[ Nat] means ( f is_differentiable_on $1,Z implies (diff ((r (#) f),Z)) . $1 = r (#) ((diff (f,Z)) . $1) );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
assume A3: f is_differentiable_on k + 1,Z ; :: thesis: (diff ((r (#) f),Z)) . (k + 1) = r (#) ((diff (f,Z)) . (k + 1))
A4: (diff (f,Z)) . k is_differentiable_on Z by A3;
k < k + 1 by NAT_1:19;
then (diff ((r (#) f),Z)) . (k + 1) = (r (#) ((diff (f,Z)) . k)) `| Z by A2, A3, TAYLOR_1:23, TAYLOR_1:def 5
.= r (#) (((diff (f,Z)) . k) `| Z) by A4, FDIFF_2:19
.= r (#) ((diff (f,Z)) . (k + 1)) by TAYLOR_1:def 5 ;
hence (diff ((r (#) f),Z)) . (k + 1) = r (#) ((diff (f,Z)) . (k + 1)) ; :: thesis: verum

end;

A5: S₁[ 0 ]

proof

assume f is_differentiable_on 0 ,Z ; :: thesis: (diff ((r (#) f),Z)) . 0 = r (#) ((diff (f,Z)) . 0)
(diff ((r (#) f),Z)) . 0 = (r (#) f) | Z by TAYLOR_1:def 5
.= r (#) (f | Z) by RFUNCT_1:49
.= r (#) ((diff (f,Z)) . 0) by TAYLOR_1:def 5 ;
hence (diff ((r (#) f),Z)) . 0 = r (#) ((diff (f,Z)) . 0) ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A1);
hence ( f is_differentiable_on n,Z implies (diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n) ) ; :: thesis: verum