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

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