theorem Th12: :: MATRIX15:12

for K being Field
for A being Matrix of K
for N being finite without_zero Subset of NAT st N c= Seg (width A) & ( for i being Nat st i in (Seg (width A)) \ N holds
Col (A,i) = (len A) |-> (0. K) ) holds
the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))