theorem :: EUCLID_8:48

for f1, f2, f3 being PartFunc of REAL,REAL
for t being Real holds (VFunc (f1,f2,f3)) . t = (((f1 . t) * <e1>) + ((f2 . t) * <e2>)) + ((f3 . t) * <e3>)