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 )
set L = (len A) |-> (0. K);
A1: len ((len A) |-> (0. K)) = len A by CARD_1:def 7;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
assume A2: ( width A <> 0 or len A = 0 ) ; :: thesis: not Solutions_of (A,((len A) |-> (0. K))) is empty
per cases ( len A = 0 or width A > 0 ) by A2;
suppose len A = 0 ; :: thesis: not Solutions_of (A,((len A) |-> (0. K))) is empty
then Solutions_of (A9,(ColVec2Mx ((len A) |-> (0. K)))) = {{}} by A1, Th51;
then A3: {} in Solutions_of (A9,(ColVec2Mx ((len A) |-> (0. K)))) by TARSKI:def 1;
then consider f being FinSequence of K such that
A4: {} = ColVec2Mx f and
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
ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;
then ( len (ColVec2Mx ((len A) |-> (0. K))) = len ((len A) |-> (0. K)) & the_rank_of A = the_rank_of (A ^^ (ColVec2Mx ((len A) |-> (0. K)))) ) by Th23, MATRIX_0:def 2;
then not Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) is empty by A1, A5, Th57;
then consider x being object such that
A6: x in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) ;
consider f being FinSequence of K such that
A7: x = ColVec2Mx f and
len f = width A by A6, Th58;
f in Solutions_of (A,((len A) |-> (0. K))) by A6, A7;
hence not Solutions_of (A,((len A) |-> (0. K))) is empty ; :: thesis: verum
end;
end;