theorem Th110: :: MATRIX13:110
for m, n being Nat
for K being Field
for M being Matrix of m,n,K st the_rank_of M = m holds
lines M is linearly-independent