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 & len X = width A & width X = width (ColVec2Mx b) & A * X = ColVec2Mx b ) by A1;

per cases ( len X = 0 or len X > 0 ) ;

suppose A3: 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_1:def 3;
hence ( x = ColVec2Mx f & len f = width A ) by A2, A3, CARD_2:83; :: thesis: verum

end;

suppose A4: len X > 0 ; :: thesis: ex f being FinSequence of K st
( x = ColVec2Mx f & len f = width A )

then ( len A <> 0 & len A = len (ColVec2Mx b) ) by A1, A2, Th33, MATRIX_1:def 4;
then len b <> 0 by MATRIX_1:def 3;
then len b > 0 ;
then A5: width X = 1 by A2, MATRIX_1:24;
take f = Col X,1; :: thesis: ( x = ColVec2Mx f & len f = width A )
thus ( x = ColVec2Mx f & len f = width A ) by A2, A4, A5, Th26, MATRIX_1:def 9; :: thesis: verum

end;

end;