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:34; :: thesis: verum