theorem Th10: :: MATRIX15:10

for K being Field
for A being Matrix of K
for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] c= Indices A holds
for i, j being Nat st i in (dom A) \ P & j in (Seg (width A)) \ Q & A * (i,j) <> 0. K & Q c= Q9 & (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q))