let r be Real; for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds
VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = (((r * (diff (f1,t0))) * <e1>) + ((r * (diff (f2,t0))) * <e2>)) + ((r * (diff (f3,t0))) * <e3>)
let f1, f2, f3 be PartFunc of REAL,REAL; for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 holds
VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = (((r * (diff (f1,t0))) * <e1>) + ((r * (diff (f2,t0))) * <e2>)) + ((r * (diff (f3,t0))) * <e3>)
let t0 be Real; ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 implies VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = (((r * (diff (f1,t0))) * <e1>) + ((r * (diff (f2,t0))) * <e2>)) + ((r * (diff (f3,t0))) * <e3>) )
assume
( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 )
; VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = (((r * (diff (f1,t0))) * <e1>) + ((r * (diff (f2,t0))) * <e2>)) + ((r * (diff (f3,t0))) * <e3>)
then VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) =
r * (VFuncdiff (f1,f2,f3,t0))
by Th90
.=
r * ((((diff (f1,t0)) * <e1>) + ((diff (f2,t0)) * <e2>)) + ((diff (f3,t0)) * <e3>))
by Th31
.=
r * ((|[(diff (f1,t0)),0,0]| + ((diff (f2,t0)) * <e2>)) + ((diff (f3,t0)) * <e3>))
by Th21
.=
r * ((|[(diff (f1,t0)),0,0]| + |[0,(diff (f2,t0)),0]|) + ((diff (f3,t0)) * <e3>))
by Th22
.=
r * ((|[(diff (f1,t0)),0,0]| + |[0,(diff (f2,t0)),0]|) + |[0,0,(diff (f3,t0))]|)
by Th23
.=
r * (|[((diff (f1,t0)) + 0),(0 + (diff (f2,t0))),(0 + 0)]| + |[0,0,(diff (f3,t0))]|)
by Lm8
.=
r * |[((diff (f1,t0)) + 0),((diff (f2,t0)) + 0),(0 + (diff (f3,t0)))]|
by Lm8
.=
(((r * (diff (f1,t0))) * <e1>) + ((r * (diff (f2,t0))) * <e2>)) + ((r * (diff (f3,t0))) * <e3>)
by Th32
;
hence
VFuncdiff ((r (#) f1),(r (#) f2),(r (#) f3),t0) = (((r * (diff (f1,t0))) * <e1>) + ((r * (diff (f2,t0))) * <e2>)) + ((r * (diff (f3,t0))) * <e3>)
; verum