let p be Element of REAL 3; :: thesis: 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 ) )
let f1, f2, f3 be PartFunc of REAL,REAL; :: thesis: for t being Real holds
( p = (VFunc (f1,f2,f3)) . t iff ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t ) )
let t be Real; :: thesis: ( p = (VFunc (f1,f2,f3)) . t iff ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t ) )
thus ( p = (VFunc (f1,f2,f3)) . t implies ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t ) ) :: thesis: ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t implies p = (VFunc (f1,f2,f3)) . t )

proof

assume p = (VFunc (f1,f2,f3)) . t ; :: thesis: ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t )
then p = |[(f1 . t),(f2 . t),(f3 . t)]| by Def5;
hence ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t ) ; :: thesis: verum

end;

assume ( p . 1 = f1 . t & p . 2 = f2 . t & p . 3 = f3 . t ) ; :: thesis: p = (VFunc (f1,f2,f3)) . t
then p = |[(f1 . t),(f2 . t),(f3 . t)]| by Th1;
hence p = (VFunc (f1,f2,f3)) . t by Def5; :: thesis: verum