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