theorem Th50: :: MATRIX13:50

for D being non empty set
for j being Nat
for A being Matrix of D
for Q being finite without_zero Subset of NAT st j in Seg (card Q) holds
Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j))