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