let K be Field; :: thesis:
let A be Matrix of K; :: thesis:
assume A1: ( width A = 0 implies len A = 0 ) ; :: thesis:
set W = width A;
set L = len A;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

per cases ;

suppose A2: the_rank_of A = 0 ; :: thesis:

dim ((width A) -VectSp_over K) = width A by MATRIX13:112;
hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A1, A2, Th63; :: thesis:

end;

suppose A3: the_rank_of A > 0 ; :: thesis:

defpred S₁[ set , set ] means for A1 being Matrix of len A, width A,K st A1 = $1 holds
Space_of_Solutions_of A9 = Space_of_Solutions_of A1;
deffunc H₁( Matrix of len A, width A,K, Nat, Nat, Element of K) -> Matrix of len A, width A,K = $1;
A4: width A > 0 by A3, MATRIX13:74;
A5: for A1, B1 being Matrix of len A, width A,K st S₁[A1,B1] holds
for a being Element of K
for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds
S₁[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H₁(B1,i,j,a)]

proof

let A1, B1 be Matrix of len A, width A,K; :: thesis:
assume A6: S₁[A1,B1] ; :: thesis:
let a be Element of K; :: thesis:
A7: dom A1 = Seg (len A1) by FINSEQ_1:def 3
.= Seg (len A) by MATRIX_0:def 2 ;
let i, j be Nat; :: thesis:
assume ( j in dom A1 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis:
then Space_of_Solutions_of (RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))) = Space_of_Solutions_of A1 by A4, A7, Th65
.= Space_of_Solutions_of A9 by A6 ;
hence S₁[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H₁(B1,i,j,a)] ; :: thesis:

end;

A8: S₁[A9,A9] ;
consider A1, B1 being Matrix of len A, width A,K, N being finite without_zero Subset of NAT such that
A9: N c= Seg (width A) and
A10: ( the_rank_of A9 = the_rank_of A1 & the_rank_of A9 = card N ) and
A11: ( S₁[A1,B1] & Segm (A1,(Seg (card N)),N) = 1. (K,(card N)) ) and
A12: for i being Nat st i in dom A1 & i > card N holds
Line (A1,i) = (width A) |-> (0. K) and
for i, j being Nat st i in Seg (card N) & j in Seg (width A1) & j < (Sgm N) . i holds
A1 * (i,j) = 0. K from MATRIX15:sch 2(A8, A5);
A13: 0 < len A by A3, MATRIX13:74;
then A14: width A1 = width A by MATRIX_0:23;
then A15: card (Seg (width A1)) = width A by FINSEQ_1:57;
then A16: card ((Seg (width A)) \ N) = (width A) - (card N) by A9, A14, CARD_2:44;
set SN = Segm (A1,(Seg (card N)),(Seg (width A1)));
A17: Seg (card N) c= Seg (card N) ;
A18: (width A) -' (card N) = (width A) - (card N) by A9, A14, A15, NAT_1:43, XREAL_1:233;
Sgm (Seg (card N)) = idseq (card N) by FINSEQ_3:48
.= id (Seg (card N)) ;
then A19: Seg (card N) = (Sgm (Seg (card N))) " (Seg (card N)) by A17, FUNCT_2:94;
Sgm (Seg (width A1)) = idseq (width A1) by FINSEQ_3:48
.= id (Seg (width A1)) ;
then N = (Sgm (Seg (width A1))) " N by A9, A14, FUNCT_2:94;
then A20: Segm ((Segm (A1,(Seg (card N)),(Seg (width A1)))),(Seg (card N)),N) = 1. (K,(card N)) by A9, A11, A14, A19, MATRIX13:56;
A21: card (Seg (card N)) = card N by FINSEQ_1:57;
A22: Seg (len A1) = dom A1 by FINSEQ_1:def 3;

A23: now :: thesis:

let i be Nat; :: thesis:
assume A24: i in (dom A1) \ (Seg (card N)) ; :: thesis:
not i in Seg (card N) by A24, XBOOLE_0:def 5;
then A25: ( i < 1 or i > card N ) ;
i in dom A1 by A24, XBOOLE_0:def 5;
hence Line (A1,i) = (width A1) |-> (0. K) by A12, A22, A14, A25, FINSEQ_1:1; :: thesis:

end;

card N <= len A1 by A10, MATRIX13:74;
then A26: Seg (card N) c= Seg (len A1) by FINSEQ_1:5;
width A1 > 0 by A4, A13, MATRIX_0:23;
then A27: Space_of_Solutions_of (Segm (A1,(Seg (card N)),(Seg (width A1)))) = Space_of_Solutions_of A1 by A3, A10, A26, A22, A23, Th66
.= Space_of_Solutions_of A9 by A11 ;

per cases ) -' (card N) = 0 or (width A) -' (card N) > 0 ) ;

suppose A28: (width A) -' (card N) = 0 ; :: thesis:

then Segm (A1,(Seg (card N)),(Seg (width A1))) = 1. (K,(card N)) by A9, A11, A14, A21, A18, CARD_2:102;
hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A10, A27, A18, A28, Lm8; :: thesis:

end;

suppose A29: (width A) -' (card N) > 0 ; :: thesis:

then ((width A) -' (card N)) + 0 > 0 ;
then (width A) -' (card N) >= 1 by NAT_1:19;
then A30: Det (1. (K,((width A) -' (card N)))) = 1_ K by MATRIX_7:16;
A31: ( card (Seg ((width A) -' (card N))) = (width A) -' (card N) & 0. K <> 1_ K ) by FINSEQ_1:57;
consider MVectors being Matrix of (width A) -' (card N), width A,K such that
A32: Segm (MVectors,(Seg ((width A) -' (card N))),((Seg (width A)) \ N)) = 1. (K,((width A) -' (card N))) and
Segm (MVectors,(Seg ((width A) -' (card N))),N) = - ((Segm ((Segm (A1,(Seg (card N)),(Seg (width A1)))),(Seg (card N)),((Seg (width A)) \ N))) @) and
A33: Lin (lines MVectors) = Space_of_Solutions_of A9 by A3, A9, A10, A27, A21, A15, A20, A29, Th67;
len MVectors = (width A) -' (card N) by A29, MATRIX_0:23;
then A34: (width A) -' (card N) >= the_rank_of MVectors by MATRIX13:74;
A35: (Seg (width A)) \ N c= Seg (width A) by XBOOLE_1:36;
Indices MVectors = [:(Seg ((width A) -' (card N))),(Seg (width A)):] by A29, MATRIX_0:23;
then A36: [:(Seg ((width A) -' (card N))),((Seg (width A)) \ N):] c= Indices MVectors by A35, ZFMISC_1:95;
reconsider B = lines MVectors as Subset of ((width A) -VectSp_over K) ;
A37: ( dom MVectors = Seg (len MVectors) & len MVectors = (width A) -' (card N) ) by FINSEQ_1:def 3, MATRIX_0:def 2;
EqSegm (MVectors,(Seg ((width A) -' (card N))),((Seg (width A)) \ N)) = 1. (K,((width A) -' (card N))) by A16, A18, A32, FINSEQ_1:57, MATRIX13:def 3;
then A38: (width A) -' (card N) <= the_rank_of MVectors by A16, A18, A36, A30, A31, MATRIX13:def 4;
then MVectors is without_repeated_line by A34, MATRIX13:105, XXREAL_0:1;
then Seg ((width A) -' (card N)),B are_equipotent by A37, WELLORD2:def 4;
then A39: card B = card (Seg ((width A) -' (card N))) by CARD_1:5
.= (width A) -' (card N) by FINSEQ_1:57 ;
the_rank_of MVectors = (width A) -' (card N) by A38, A34, XXREAL_0:1;
then lines MVectors is linearly-independent by MATRIX13:121;
hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A10, A18, A33, A39, VECTSP_9:26; :: thesis:

end;

end;

end;

end;