let K be Field; :: thesis: for A being Matrix of K
for b being FinSequence of K
for x being set st x in Solutions_of (A,()) holds
ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )

let A be Matrix of K; :: thesis: for b being FinSequence of K
for x being set st x in Solutions_of (A,()) holds
ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )

let b be FinSequence of K; :: thesis: for x being set st x in Solutions_of (A,()) holds
ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )

let x be set ; :: thesis: ( x in Solutions_of (A,()) implies ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A ) )

assume A1: x in Solutions_of (A,()) ; :: thesis: 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 () and
A * X = ColVec2Mx b by A1;
per cases ( len X = 0 or len X > 0 ) ;
suppose A5: len X = 0 ; :: thesis: ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )

take f = 0 |-> (0. K); :: thesis: ( x = ColVec2Mx f & len f = width A )
len () = 0 by MATRIX_0:def 2;
hence ( x = ColVec2Mx f & len f = width A ) by ; :: thesis: verum
end;
suppose A6: len X > 0 ; :: thesis: ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )

take Col (X,1) ; :: thesis: ( x = ColVec2Mx (Col (X,1)) & len (Col (X,1)) = width A )
A7: len A = len () by ;
len A <> 0 by ;
then len b > 0 by ;
then width X = 1 by ;
hence ( x = ColVec2Mx (Col (X,1)) & len (Col (X,1)) = width A ) by ; :: thesis: verum
end;
end;