:: deftheorem DEF1 defines F2M ANPROJ_8:def 1 :
for D being non empty set
for p being FinSequence of D st len p = 3 holds
F2M p = <*<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>*>;