not Solutions_of A,((len A) |-> (0. K)) is empty by A1, Th61;
hence ex b₁ being strict Subspace of (width A) -VectSp_over K st the carrier of b₁ = Solutions_of A,((len A) |-> (0. K)) by VECTSP_4:42; :: thesis: verum