let K be Field; :: thesis: for A being Matrix of K
for b being FinSequence of K st not Solutions_of A,b is empty & width A = 0 holds
len A = 0
let A be Matrix of K; :: thesis: for b being FinSequence of K st not Solutions_of A,b is empty & width A = 0 holds
len A = 0
let b be FinSequence of K; :: thesis: ( not Solutions_of A,b is empty & width A = 0 implies len A = 0 )
set S = Solutions_of A,b;
assume A1: ( not Solutions_of A,b is empty & width A = 0 ) ; :: thesis: len A = 0
then consider x being set such that
A2: x in Solutions_of A,b by XBOOLE_0:def 1;
consider f being FinSequence of K such that
A3: ( x = f & ColVec2Mx f in Solutions_of A,(ColVec2Mx b) ) by A2;
consider X being Matrix of K such that
A4: ( ColVec2Mx f = X & len X = width A & width X = width (ColVec2Mx b) ) and
A5: A * X = ColVec2Mx b by A3;
width (A * X) = width X by A4, MATRIX_3:def 4
.= 0 by A1, A4, MATRIX_1:def 4 ;
then len b <= 0 by A5, MATRIX_1:24;
hence 0 = len b
.= len (ColVec2Mx b) by MATRIX_1:def 3
.= len A by A3, Th33 ;
:: thesis: verum