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 object such that
A3: x in Solutions_of (A,b) by A1;
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_0:def 3 ;
hence 0 = len b by A6, MATRIX_0:23
.= len (ColVec2Mx b) by MATRIX_0:def 2
.= len A by A4, Th33 ;
:: thesis: verum