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:106;
then B4: width A <> 0 ;
set L = Line ((1. (K,(width A))),j);
A5: width (1. (K,(width A))) = width A by MATRIX_1:25;
then A6: dom (Line ((1. (K,(width A))),j)) = Seg (width A) by FINSEQ_2:144;
A7: Indices (1. (K,(width A))) = [:(Seg (width A)),(Seg (width A)):] by MATRIX_1:25;

A8: 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
A9: k in dom (Line ((1. (K,(width A))),j)) and
A10: k <> j ; :: thesis: 0. K = (Line ((1. (K,(width A))),j)) . k
[j,k] in Indices (1. (K,(width A))) by A4, A6, A7, A9, ZFMISC_1:106;
hence 0. K = (1. (K,(width A))) * (j,k) by A10, MATRIX_1:def 12
.= (Line ((1. (K,(width A))),j)) . k by A5, A6, A9, MATRIX_1:def 8 ;
:: thesis: verum

end;

A11: dom (Line (A,i)) = Seg (width A) by FINSEQ_2:144;
[j,j] in Indices (1. (K,(width A))) by A4, A7, ZFMISC_1:106;
then 1_ K = (1. (K,(width A))) * (j,j) by MATRIX_1:def 12
.= (Line ((1. (K,(width A))),j)) . j by A4, A5, MATRIX_1:def 8 ;
then A12: Sum (mlt ((Line ((1. (K,(width A))),j)),(Line (A,i)))) = (Line (A,i)) . j by A4, A6, A11, A8, MATRIX_3:19
.= A * (i,j) by A4, MATRIX_1:def 8 ;
A13: ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;
A14: i in dom A by A2, ZFMISC_1:106;
Line ((1. (K,(width A))),j) in (width A) -tuples_on the carrier of K by A5;
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, B4;
then consider f being FinSequence of K such that
A15: f = Line ((1. (K,(width A))),j) and
A16: ColVec2Mx f in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) ;
consider X being Matrix of K such that
A17: X = ColVec2Mx f and
A18: len X = width A and
width X = width (ColVec2Mx ((len A) |-> (0. K))) and
A19: A * X = ColVec2Mx ((len A) |-> (0. K)) by A16;
A20: 1 in Seg 1 ;
A21: dom A = Seg (len A) by FINSEQ_1:def 3;
then len A <> 0 by A2, ZFMISC_1:106;
then Indices (ColVec2Mx ((len A) |-> (0. K))) = [:(Seg (len A)),(Seg 1):] by A13, MATRIX_1:24;
then A22: [i,1] in Indices (ColVec2Mx ((len A) |-> (0. K))) by A14, A21, A20, ZFMISC_1:106;
then (Line (A,i)) "*" (Col (X,1)) = (0. (K,(len A),1)) * (i,1) by A18, A19, A13, MATRIX_3:def 4
.= 0. K by A13, A22, MATRIX_3:3 ;
then 0. K = (Col (X,1)) "*" (Line (A,i)) by FVSUM_1:115
.= Sum (mlt (f,(Line (A,i)))) by A17, A18, Th26, B4 ;
hence contradiction by A3, A15, A12; :: thesis: verum