for m, n being Nat
for K being Field
for M being Matrix of m,n,K st the_rank_of M = m holds
M is without_repeated_line