let K be Field; :: thesis: for A being Matrix of K st Space_of_Solutions_of A = (width A) -VectSp_over K holds
the_rank_of A = 0
let A be Matrix of K; :: thesis: ( Space_of_Solutions_of A = (width A) -VectSp_over K implies the_rank_of A = 0 )
assume A1: Space_of_Solutions_of A = (width A) -VectSp_over K ; :: thesis: the_rank_of A = 0
assume the_rank_of A <> 0 ; :: thesis: contradiction
then consider i, j being Nat such that
A2: [i,j] in Indices A and
A3: A * (i,j) <> 0. K by MATRIX13:94;
A4: j in Seg (width A) by A2, ZFMISC_1:87;
then A5: width A <> 0 ;
set L = Line ((1. (K,(width A))),j);
A6: width (1. (K,(width A))) = width A by MATRIX_1:24;
then A7: dom (Line ((1. (K,(width A))),j)) = Seg (width A) by FINSEQ_2:124;
A8: Indices (1. (K,(width A))) = [:(Seg (width A)),(Seg (width A)):] by MATRIX_1:24;

A9: now

let k be Nat; :: thesis: ( k in dom (Line ((1. (K,(width A))),j)) & k <> j implies 0. K = (Line ((1. (K,(width A))),j)) . k )
assume that
A10: k in dom (Line ((1. (K,(width A))),j)) and
A11: k <> j ; :: thesis: 0. K = (Line ((1. (K,(width A))),j)) . k
[j,k] in Indices (1. (K,(width A))) by A4, A7, A8, A10, ZFMISC_1:87;
hence 0. K = (1. (K,(width A))) * (j,k) by A11, MATRIX_1:def 11
.= (Line ((1. (K,(width A))),j)) . k by A6, A7, A10, MATRIX_1:def 7 ;
:: thesis: verum

end;

A12: dom (Line (A,i)) = Seg (width A) by FINSEQ_2:124;
[j,j] in Indices (1. (K,(width A))) by A4, A8, ZFMISC_1:87;
then 1_ K = (1. (K,(width A))) * (j,j) by MATRIX_1:def 11
.= (Line ((1. (K,(width A))),j)) . j by A4, A6, MATRIX_1:def 7 ;
then A13: Sum (mlt ((Line ((1. (K,(width A))),j)),(Line (A,i)))) = (Line (A,i)) . j by A4, A7, A12, A9, MATRIX_3:17
.= A * (i,j) by A4, MATRIX_1:def 7 ;
A14: ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;
A15: i in dom A by A2, ZFMISC_1:87;
Line ((1. (K,(width A))),j) in (width A) -tuples_on the carrier of K by A6;
then Line ((1. (K,(width A))),j) in the carrier of (Space_of_Solutions_of A) by A1, MATRIX13:102;
then Line ((1. (K,(width A))),j) in Solutions_of (A,((len A) |-> (0. K))) by Def5, A5;
then consider f being FinSequence of K such that
A16: f = Line ((1. (K,(width A))),j) and
A17: ColVec2Mx f in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) ;
consider X being Matrix of K such that
A18: X = ColVec2Mx f and
A19: len X = width A and
width X = width (ColVec2Mx ((len A) |-> (0. K))) and
A20: A * X = ColVec2Mx ((len A) |-> (0. K)) by A17;
A21: 1 in Seg 1 ;
A22: dom A = Seg (len A) by FINSEQ_1:def 3;
then len A <> 0 by A2, ZFMISC_1:87;
then Indices (ColVec2Mx ((len A) |-> (0. K))) = [:(Seg (len A)),(Seg 1):] by A14, MATRIX_1:23;
then A23: [i,1] in Indices (ColVec2Mx ((len A) |-> (0. K))) by A15, A22, A21, ZFMISC_1:87;
then (Line (A,i)) "*" (Col (X,1)) = (0. (K,(len A),1)) * (i,1) by A19, A20, A14, MATRIX_3:def 4
.= 0. K by A14, A23, MATRIX_3:1 ;
then 0. K = (Col (X,1)) "*" (Line (A,i)) by FVSUM_1:90
.= Sum (mlt (f,(Line (A,i)))) by A18, A19, Th26, A5 ;
hence contradiction by A3, A16, A13; :: thesis: verum