let f1, f2, f3, g1, g2, g3 be 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
let t1, t2 be Real; ( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 implies (VFunc (f1,f2,f3)) . t1 = (VFunc (g1,g2,g3)) . t2 )
assume A1:
( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 )
; (VFunc (f1,f2,f3)) . t1 = (VFunc (g1,g2,g3)) . t2
set p = |[(f1 . t1),(f2 . t1),(f3 . t1)]|;
set q = |[(g1 . t2),(g2 . t2),(g3 . t2)]|;
( |[(f1 . t1),(f2 . t1),(f3 . t1)]| = (VFunc (f1,f2,f3)) . t1 & |[(g1 . t2),(g2 . t2),(g3 . t2)]| = (VFunc (g1,g2,g3)) . t2 )
by Def5;
hence
(VFunc (f1,f2,f3)) . t1 = (VFunc (g1,g2,g3)) . t2
by A1; verum