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

.= 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:31; :: thesis: verum

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

then the carrier of ((width A) -VectSp_over K) =
Solutions_of (A,((len A) |-> (0. K)))
let x be object ; :: 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;

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

end;

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_0:def 3;

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:94 ;

then x = <*> the carrier of K by A3, TARSKI:def 1;

then f = x by A5, A8, MATRIX_0:def 3;

hence x in Solutions_of (A,((len A) |-> (0. K))) by A6, A7; :: thesis: verum

end;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_0:def 3;

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:94 ;

then x = <*> the carrier of K by A3, TARSKI:def 1;

then f = x by A5, A8, MATRIX_0:def 3;

hence x in Solutions_of (A,((len A) |-> (0. K))) by A6, A7; :: thesis: verum

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

.= 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:31; :: thesis: verum