theorem Th41: :: EUCLID_8:49

for p being Element of REAL 3
for f1, f2, f3 being PartFunc of REAL,REAL
for t being Real holds
( p = (VFunc (f1,f2,f3)) . t iff ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t ) )