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