let K be Field; :: thesis: for A being Matrix of K st ( width A = 0 implies len A = 0 ) & the_rank_of A = 0 holds
Space_of_Solutions_of A = (width A) -VectSp_over K
let A be Matrix of K; :: thesis: ( ( width A = 0 implies len A = 0 ) & the_rank_of A = 0 implies Space_of_Solutions_of A = (width A) -VectSp_over K )
assume that
A1: ( width A = 0 implies len A = 0 ) and
A2: the_rank_of A = 0 ; :: thesis: Space_of_Solutions_of A = (width A) -VectSp_over K
set L = (len A) |-> (0. K);
the carrier of ((width A) -VectSp_over K) c= Solutions_of A,((len A) |-> (0. K))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of ((width A) -VectSp_over K) or x in Solutions_of A,((len A) |-> (0. K)) )
assume A3: x in the carrier of ((width A) -VectSp_over K) ; :: thesis: x in Solutions_of A,((len A) |-> (0. K))
reconsider x9 = x as Element of (width A) -tuples_on the carrier of K by A3, MATRIX13:102;
A4: ( A = 0. K,(len A),(width A) & ColVec2Mx ((len A) |-> (0. K)) = 0. K,(len A),1 ) by A2, Th32, MATRIX13:95;

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

suppose A5: len A = 0 ; :: thesis: x in Solutions_of A,((len A) |-> (0. K))

then Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) = {{} } by A4, Th51;
then A6: {} in Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) by TARSKI:def 1;
then consider f being FinSequence of K such that
A7: {} = ColVec2Mx f and
A8: len f = width A by Th58;
width A = 0 by A5, MATRIX_1:def 4;
then the carrier of ((width A) -VectSp_over K) = 0 -tuples_on the carrier of K by MATRIX13:102
.= {(<*> the carrier of K)} by FINSEQ_2:112 ;
then x = <*> the carrier of K by A3, TARSKI:def 1;
then f = x by A5, A8, MATRIX_1:def 4;
hence x in Solutions_of A,((len A) |-> (0. K)) by A6, A7; :: thesis: verum

end;

suppose A9: len A > 0 ; :: thesis: x in Solutions_of A,((len A) |-> (0. K))

A10: len x9 = width A by FINSEQ_1:def 18;
Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) = { X where X is Matrix of width A,1,K : verum } by A1, A4, A9, Th54;
then ColVec2Mx x9 in Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) by A10;
hence x in Solutions_of A,((len A) |-> (0. K)) ; :: thesis: verum

end;

end;

end;

then the carrier of ((width A) -VectSp_over K) = Solutions_of A,((len A) |-> (0. K)) by XBOOLE_0:def 10
.= the carrier of (Space_of_Solutions_of A) by A1, Def5 ;
hence Space_of_Solutions_of A = (width A) -VectSp_over K by VECTSP_4:39; :: thesis: verum