theorem :: MATRIX15:64

for K being Field
for A being Matrix of K st Space_of_Solutions_of A = (width A) -VectSp_over K holds
the_rank_of A = 0