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 the_rank_of A > 0 ;
then consider i, j being Nat such that
A2: ( [i,j] in Indices A & A * i,j <> 0. K ) by MATRIX13:94;
A3: ( j in Seg (width A) & i in dom A & dom A = Seg (len A) ) by A2, FINSEQ_1:def 3, ZFMISC_1:106;
then A4: ( width A <> 0 & len A <> 0 ) ;
set L = Line (1. K,(width A)),j;
A5: width (1. K,(width A)) = width A by MATRIX_1:25;
then Line (1. K,(width A)),j in (width A) -tuples_on the carrier of K ;
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, A3, FINSEQ_1:4;
then consider f being FinSequence of K such that
A6: ( f = Line (1. K,(width A)),j & ColVec2Mx f in Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) ) ;
consider X being Matrix of K such that
A7: ( X = ColVec2Mx f & len X = width A ) and
width X = width (ColVec2Mx ((len A) |-> (0. K))) and
A8: A * X = ColVec2Mx ((len A) |-> (0. K)) by A6;
A9: ( len A > 0 & ColVec2Mx ((len A) |-> (0. K)) = 0. K,(len A),1 ) by Th32, A4;
then ( Indices (ColVec2Mx ((len A) |-> (0. K))) = [:(Seg (len A)),(Seg 1):] & 1 in Seg 1 ) by MATRIX_1:24;
then A10: [i,1] in Indices (ColVec2Mx ((len A) |-> (0. K))) by A3, ZFMISC_1:106;
then (Line A,i) "*" (Col X,1) = (0. K,(len A),1) * i,1 by A7, A8, A9, MATRIX_3:def 4
.= 0. K by A10, A9, MATRIX_3:3 ;
then A11: 0. K = (Col X,1) "*" (Line A,i) by FVSUM_1:115
.= Sum (mlt f,(Line A,i)) by A3, A7, Th26, FINSEQ_1:4 ;
A12: ( dom (Line (1. K,(width A)),j) = Seg (width A) & dom (Line A,i) = Seg (width A) ) by A5, FINSEQ_2:144;
A13: Indices (1. K,(width A)) = [:(Seg (width A)),(Seg (width A)):] by MATRIX_1:25;
then [j,j] in Indices (1. K,(width A)) by A3, ZFMISC_1:106;
then A14: 1_ K = (1. K,(width A)) * j,j by MATRIX_1:def 12
.= (Line (1. K,(width A)),j) . j by A3, A5, MATRIX_1:def 8 ;

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 A15: ( k in dom (Line (1. K,(width A)),j) & k <> j ) ; :: thesis: 0. K = (Line (1. K,(width A)),j) . k
[j,k] in Indices (1. K,(width A)) by A13, A3, A12, A15, ZFMISC_1:106;
hence 0. K = (1. K,(width A)) * j,k by A15, MATRIX_1:def 12
.= (Line (1. K,(width A)),j) . k by A5, A12, A15, MATRIX_1:def 8 ;
:: thesis: verum

end;

then Sum (mlt (Line (1. K,(width A)),j),(Line A,i)) = (Line A,i) . j by A3, A12, A14, MATRIX_3:19
.= A * i,j by A3, MATRIX_1:def 8 ;
hence contradiction by A11, A6, A2; :: thesis: verum