theorem :: EUCLID_8:104

for r being 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>)