let K be Field; for A being Matrix of K
for b being FinSequence of K
for x being set st x in Solutions_of (A,(ColVec2Mx b)) holds
ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )
let A be Matrix of K; for b being FinSequence of K
for x being set st x in Solutions_of (A,(ColVec2Mx b)) holds
ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )
let b be FinSequence of K; for x being set st x in Solutions_of (A,(ColVec2Mx b)) holds
ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )
let x be set ; ( x in Solutions_of (A,(ColVec2Mx b)) implies ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A ) )
assume A1:
x in Solutions_of (A,(ColVec2Mx b))
; ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )
consider X being Matrix of K such that
A2:
X = x
and
A3:
len X = width A
and
A4:
width X = width (ColVec2Mx b)
and
A * X = ColVec2Mx b
by A1;
per cases
( len X = 0 or len X > 0 )
;
suppose A6:
len X > 0
;
ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )take
Col (
X,1)
;
( x = ColVec2Mx (Col (X,1)) & len (Col (X,1)) = width A )A7:
len A = len (ColVec2Mx b)
by A1, Th33;
len A <> 0
by A3, A6, MATRIX_0:def 3;
then
len b > 0
by A7, MATRIX_0:def 2;
then
width X = 1
by A4, MATRIX_0:23;
hence
(
x = ColVec2Mx (Col (X,1)) &
len (Col (X,1)) = width A )
by A2, A3, A6, Th26, MATRIX_0:def 8;
verum end; end;