theorem :: ANPROJ_8:81

for D being non empty set
for pf being FinSequence of D st len pf = 3 holds
<*(Col (<*pf*>,1)),(Col (<*pf*>,2)),(Col (<*pf*>,3))*> = F2M pf