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 that
A1: not Solutions_of A,b is empty and
A2: width A = 0 ; :: thesis: len A = 0
consider x being set such that
A3: x in Solutions_of A,b by A1, XBOOLE_0:def 1;
consider f being FinSequence of K such that
x = f and
A4: ColVec2Mx f in Solutions_of A,(ColVec2Mx b) by A3;
consider X being Matrix of K such that
ColVec2Mx f = X and
A5: len X = width A and
width X = width (ColVec2Mx b) and
A6: A * X = ColVec2Mx b by A4;
width (A * X) = width X by A5, MATRIX_3:def 4
.= 0 by A2, A5, MATRIX_1:def 4 ;
hence 0 = len b by A6, MATRIX_1:24
.= len (ColVec2Mx b) by MATRIX_1:def 3
.= len A by A4, Th33 ;
:: thesis: verum