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
(diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n)
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
(diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n)
let Z be 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 f be PartFunc of REAL,REAL; ( f is_differentiable_on n,Z implies (diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n) )
defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[k + 1]
assume A3:
f is_differentiable_on k + 1,
Z
;
(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))
;
verum
end;
A5:
S1[ 0 ]
for k being Nat holds S1[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) )
; verum