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