theorem Th73: :: MATRIX13:73

for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
( card P <= len M & card Q <= width M )