let K be Field; :: thesis: for A being Matrix of K st Space_of_Solutions_of A = () -VectSp_over K holds
the_rank_of A = 0

let A be Matrix of K; :: thesis: ( Space_of_Solutions_of A = () -VectSp_over K implies the_rank_of A = 0 )
assume A1: Space_of_Solutions_of A = () -VectSp_over K ; :: thesis:
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 () by ;
then A5: width A <> 0 ;
set L = Line ((1. (K,())),j);
A6: width (1. (K,())) = width A by MATRIX_0:24;
then A7: dom (Line ((1. (K,())),j)) = Seg () by FINSEQ_2:124;
A8: Indices (1. (K,())) = [:(Seg ()),(Seg ()):] by MATRIX_0:24;
A9: now :: thesis: for k being Nat st k in dom (Line ((1. (K,())),j)) & k <> j holds
0. K = (Line ((1. (K,())),j)) . k
let k be Nat; :: thesis: ( k in dom (Line ((1. (K,())),j)) & k <> j implies 0. K = (Line ((1. (K,())),j)) . k )
assume that
A10: k in dom (Line ((1. (K,())),j)) and
A11: k <> j ; :: thesis: 0. K = (Line ((1. (K,())),j)) . k
[j,k] in Indices (1. (K,())) by ;
hence 0. K = (1. (K,())) * (j,k) by
.= (Line ((1. (K,())),j)) . k by ;
:: thesis: verum
end;
A12: dom (Line (A,i)) = Seg () by FINSEQ_2:124;
[j,j] in Indices (1. (K,())) by ;
then 1_ K = (1. (K,())) * (j,j) by MATRIX_1:def 3
.= (Line ((1. (K,())),j)) . j by ;
then A13: Sum (mlt ((Line ((1. (K,())),j)),(Line (A,i)))) = (Line (A,i)) . j by
.= A * (i,j) by ;
A14: ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;
A15: i in dom A by ;
Line ((1. (K,())),j) in () -tuples_on the carrier of K by A6;
then Line ((1. (K,())),j) in the carrier of by ;
then Line ((1. (K,())),j) in Solutions_of (A,((len A) |-> (0. K))) by ;
then consider f being FinSequence of K such that
A16: f = Line ((1. (K,())),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 ;
then Indices (ColVec2Mx ((len A) |-> (0. K))) = [:(Seg (len A)),(Seg 1):] by ;
then A23: [i,1] in Indices (ColVec2Mx ((len A) |-> (0. K))) by ;
then (Line (A,i)) "*" (Col (X,1)) = (0. (K,(len A),1)) * (i,1) by
.= 0. K by ;
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