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 = () -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 = () -VectSp_over K )
assume that
A1: ( width A = 0 implies len A = 0 ) and
A2: the_rank_of A = 0 ; :: thesis:
set L = (len A) |-> (0. K);
the carrier of (() -VectSp_over K) c= Solutions_of (A,((len A) |-> (0. K)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (() -VectSp_over K) or x in Solutions_of (A,((len A) |-> (0. K))) )
assume A3: x in the carrier of (() -VectSp_over K) ; :: thesis: x in Solutions_of (A,((len A) |-> (0. K)))
reconsider x9 = x as Element of () -tuples_on the carrier of K by ;
A4: ( A = 0. (K,(len A),()) & ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) ) by ;
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 ;
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 ;
then the carrier of (() -VectSp_over K) = 0 -tuples_on the carrier of K by MATRIX13:102
.= {(<*> the carrier of K)} by FINSEQ_2:94 ;
then x = <*> the carrier of K by ;
then f = x by ;
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 CARD_1:def 7;
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 (() -VectSp_over K) = Solutions_of (A,((len A) |-> (0. K)))
.= the carrier of by ;
hence Space_of_Solutions_of A = () -VectSp_over K by VECTSP_4:31; :: thesis: verum