:: deftheorem defines VFuncdiff EUCLID_8:def 7 :
for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real holds VFuncdiff (f1,f2,f3,t0) = |[(diff (f1,t0)),(diff (f2,t0)),(diff (f3,t0))]|;