theorem Th51: :: ANPROJ_8:63

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