theorem :: EUCLID_8:96

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 (f1,f2,f3,t0) = (((diff (f1,t0)) * <e1>) + ((diff (f2,t0)) * <e2>)) + ((diff (f3,t0)) * <e3>) by Th31;