let K be Field; :: thesis: for A being Matrix of K st ( width A <> 0 or len A = 0 ) holds
not Solutions_of A,((len A) |-> (0. K)) is empty
let A be Matrix of K; :: thesis: ( ( width A <> 0 or len A = 0 ) implies not Solutions_of A,((len A) |-> (0. K)) is empty )
assume A1: ( width A <> 0 or len A = 0 ) ; :: thesis: not Solutions_of A,((len A) |-> (0. K)) is empty
set L = (len A) |-> (0. K);
A2: len ((len A) |-> (0. K)) = len A by FINSEQ_1:def 18;
reconsider A' = A as Matrix of len A, width A,K by MATRIX_2:7;

per cases ( len A = 0 or width A > 0 ) by A1;

suppose len A = 0 ; :: thesis: not Solutions_of A,((len A) |-> (0. K)) is empty

then Solutions_of A',(ColVec2Mx ((len A) |-> (0. K))) = {{} } by A2, Th51;
then A3: {} in Solutions_of A',(ColVec2Mx ((len A) |-> (0. K))) by TARSKI:def 1;
then consider f being FinSequence of K such that
A4: ( {} = ColVec2Mx f & len f = width A ) by Th58;
f in Solutions_of A,((len A) |-> (0. K)) by A3, A4;
hence not Solutions_of A,((len A) |-> (0. K)) is empty ; :: thesis: verum

end;

suppose A5: width A > 0 ; :: thesis: not Solutions_of A,((len A) |-> (0. K)) is empty

A6: ( len (ColVec2Mx ((len A) |-> (0. K))) = len ((len A) |-> (0. K)) & ColVec2Mx ((len A) |-> (0. K)) = 0. K,(len A),1 ) by Th32, MATRIX_1:def 3;
then the_rank_of A = the_rank_of (A ^^ (ColVec2Mx ((len A) |-> (0. K)))) by Th23;
then not Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) is empty by A2, A5, A6, Th57;
then consider x being set such that
A7: x in Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) by XBOOLE_0:def 1;
consider f being FinSequence of K such that
A8: ( x = ColVec2Mx f & len f = width A ) by A7, Th58;
f in Solutions_of A,((len A) |-> (0. K)) by A7, A8;
hence not Solutions_of A,((len A) |-> (0. K)) is empty ; :: thesis: verum

end;

end;