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,(ColVec2Mx b)) 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,(ColVec2Mx b)) 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,(ColVec2Mx b)) 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,(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)) ; :: 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 (ColVec2Mx b) 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 (ColVec2Mx f) = 0 by MATRIX_0:def 2;
hence ( x = ColVec2Mx f & len f = width A ) by A2, A3, A5, CARD_2:64; :: 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 (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; :: thesis: verum

end;

end;