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

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;

end;

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;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

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;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