theorem Th11: :: MATRIX15:11

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