:: deftheorem Def5 defines Space_of_Solutions_of MATRIX15:def 5 :
for K being Field
for A being Matrix of K st ( width A = 0 implies len A = 0 ) holds
for b₃ being strict Subspace of (width A) -VectSp_over K holds
( b₃ = Space_of_Solutions_of A iff the carrier of b₃ = Solutions_of (A,((len A) |-> (0. K))) );