let p be FinSequence of REAL ; :: thesis: ( len p = 3 implies p is 3 -element FinSequence of REAL )
assume len p = 3 ; :: thesis: p is 3 -element FinSequence of REAL
then p = <*(p . 1),(p . 2),(p . 3)*> by FINSEQ_1:45;
hence p is 3 -element FinSequence of REAL ; :: thesis: verum