let K be Field; 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; 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; ( 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
; 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
;
verum