theorem :: MATRIX15:55

for m, n being Nat
for K being Field st n > 0 & not Solutions_of ((0. (K,n,0)),(0. (K,n,m))) is empty holds
m = 0