let p be Element of REAL 3; :: thesis: for f1, f2, f3 being PartFunc of ,
for t being Real st p = (VFunc f1,f2,f3) . t holds
( len p = 3 & dom p = Seg 3 )
let f1, f2, f3 be PartFunc of ,; :: thesis: for t being Real st p = (VFunc f1,f2,f3) . t holds
( len p = 3 & dom p = Seg 3 )
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t implies ( len p = 3 & dom p = Seg 3 ) )
assume p = (VFunc f1,f2,f3) . t ; :: thesis: ( len p = 3 & dom p = Seg 3 )
then p = |[(f1 . t),(f2 . t),(f3 . t)]| by Def1;
hence ( len p = 3 & dom p = Seg 3 ) by FINSEQ_1:62, FINSEQ_3:30; :: thesis: verum