theorem :: EUCLID_8:57

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