theorem Th59: :: ANPROJ_8:71

for k being Nat
for D being non empty set
for pf being FinSequence of D st k in dom pf holds
Col (<*pf*>,k) = <*(pf . k)*>