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