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 ( n = 0 or m = 0 ) holds
the_rank_of (Segm (M,nt,mt)) = 0