theorem :: EUCLID_8:56

for p, q being Element of REAL 3
for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t1, t2 being Real st p = (VFunc (f1,f2,f3)) . t1 & q = (VFunc (g1,g2,g3)) . t2 & p = q holds
( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 )