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;

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 )
;

end;

suppose A5:
len X = 0
; :: thesis: ex f being FinSequence of K st

( x = ColVec2Mx f & len f = width A )

( 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;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

suppose A6:
len X > 0
; :: thesis: ex f being FinSequence of K st

( x = ColVec2Mx f & len f = width A )

( 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;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