theorem Th94: :: MATRIX13:94

for K being Field
for M being Matrix of K holds
( the_rank_of M > 0 iff ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) )