theorem Th78: :: MATRIX13:78

for m, n being Nat
for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
the_rank_of M >= the_rank_of (Segm (M,nt,mt))