theorem Th68: :: MATRIX15:68

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