let K be Field; :: thesis: for A being Matrix of K st ( width A = 0 implies len A = 0 ) holds
dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)
let A be Matrix of K; :: thesis: ( ( width A = 0 implies len A = 0 ) implies dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) )
assume A1: ( width A = 0 implies len A = 0 ) ; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)
set L = len A;
set W = width A;
reconsider A' = A as Matrix of len A, width A,K by MATRIX_2:7;

per cases ( the_rank_of A = 0 or the_rank_of A > 0 ) ;

suppose A2: the_rank_of A = 0 ; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

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: verum

end;

suppose A3: the_rank_of A > 0 ; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

deffunc H₁( Matrix of len A, width A,K, Nat, Nat, Element of K) -> Matrix of len A, width A,K = $1;
defpred S₁[ set , set ] means for A1 being Matrix of len A, width A,K st A1 = $1 holds
Space_of_Solutions_of A' = Space_of_Solutions_of A1;
A4: S₁[A',A'] ;
A5: width A > 0 by A3, MATRIX13:74;
A6: 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: ( S₁[A1,B1] implies 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)] )
assume A7: S₁[A1,B1] ; :: thesis: 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)]
let a be Element of K; :: thesis: 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)]
let i, j be Nat; :: thesis: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) implies S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)] )
assume A8: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)]
dom A1 = Seg (len A1) by FINSEQ_1:def 3
.= Seg (len A) by MATRIX_1:def 3 ;
then Space_of_Solutions_of (RLine A1,i,((Line A1,i) + (a * (Line A1,j)))) = Space_of_Solutions_of A1 by A5, A8, Th65
.= Space_of_Solutions_of A' by A7 ;
hence S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)] ; :: thesis: verum

end;

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 A' = the_rank_of A1 & the_rank_of A' = 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(A4, A6);
card N <= len A1 by A10, MATRIX13:74;
then A13: ( Seg (card N) c= Seg (len A1) & Seg (len A1) = dom A1 ) by FINSEQ_1:7, FINSEQ_1:def 3;
A14: ( not Seg (card N) is empty & card N > 0 ) by A3, A10;
A15: 0 < len A by A3, MATRIX13:74;
then A16: width A1 = width A by MATRIX_1:24;
A17: width A1 > 0 by A5, A15, MATRIX_1:24;

A18: now

let i be Nat; :: thesis: ( i in (dom A1) \ (Seg (card N)) implies Line A1,i = (width A1) |-> (0. K) )
assume A19: i in (dom A1) \ (Seg (card N)) ; :: thesis: Line A1,i = (width A1) |-> (0. K)
A20: ( i in dom A1 & not i in Seg (card N) ) by A19, XBOOLE_0:def 5;
then ( 1 <= i & ( i < 1 or i > card N ) ) by A13, FINSEQ_1:3;
hence Line A1,i = (width A1) |-> (0. K) by A12, A16, A20; :: thesis: verum

end;

set SN = Segm A1,(Seg (card N)),(Seg (width A1));
A21: Space_of_Solutions_of (Segm A1,(Seg (card N)),(Seg (width A1))) = Space_of_Solutions_of A1 by A13, A14, A17, A18, Th66
.= Space_of_Solutions_of A' by A11 ;
A22: ( card (Seg (card N)) = card N & card (Seg (width A1)) = width A ) by A16, FINSEQ_1:78;
A23: Sgm (Seg (card N)) = idseq (card N) by FINSEQ_3:54
.= id (Seg (card N)) ;
A24: Sgm (Seg (width A1)) = idseq (width A1) by FINSEQ_3:54
.= id (Seg (width A1)) ;
Seg (card N) c= Seg (card N) ;
then ( Seg (card N) = (Sgm (Seg (card N))) " (Seg (card N)) & N = (Sgm (Seg (width A1))) " N ) by A23, A24, A9, A16, FUNCT_2:171;
then A25: Segm (Segm A1,(Seg (card N)),(Seg (width A1))),(Seg (card N)),N = 1. K,(card N) by A11, A9, A16, MATRIX13:56;
A26: ( card N <= width A & card ((Seg (width A)) \ N) = (width A) - (card N) ) by A22, A16, A9, CARD_2:63, NAT_1:44;
then A27: (width A) -' (card N) = (width A) - (card N) by XREAL_1:235;

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

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

then Segm A1,(Seg (card N)),(Seg (width A1)) = 1. K,(card N) by A11, A16, A22, A9, A27, CARD_FIN:1;
hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A28, Lm8, A21, A10, A27; :: thesis: verum

end;

suppose A29: (width A) -' (card N) > 0 ; :: thesis: dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)

then consider MVectors being Matrix of (width A) -' (card N), width A,K such that
A30: 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
A31: Lin (lines MVectors) = Space_of_Solutions_of A' by A9, A22, A3, A10, Th67, A25, A21;
A32: ( dom MVectors = Seg (len MVectors) & len MVectors = (width A) -' (card N) ) by FINSEQ_1:def 3, MATRIX_1:def 3;
A33: card (Seg ((width A) -' (card N))) = (width A) -' (card N) by FINSEQ_1:78;
A34: ( Indices MVectors = [:(Seg ((width A) -' (card N))),(Seg (width A)):] & len MVectors = (width A) -' (card N) ) by A29, MATRIX_1:24;
A35: the_rank_of MVectors = (width A) -' (card N)

proof

A36: EqSegm MVectors,(Seg ((width A) -' (card N))),((Seg (width A)) \ N) = 1. K,((width A) -' (card N)) by A30, A26, A27, FINSEQ_1:78, MATRIX13:def 3;
(Seg (width A)) \ N c= Seg (width A) by XBOOLE_1:36;
then A37: [:(Seg ((width A) -' (card N))),((Seg (width A)) \ N):] c= Indices MVectors by A34, ZFMISC_1:118;
((width A) -' (card N)) + 0 > 0 by A29;
then (width A) -' (card N) >= 1 by NAT_1:19;
then ( Det (1. K,((width A) -' (card N))) = 1_ K & 0. K <> 1_ K ) by MATRIX_7:16;
then ( (width A) -' (card N) <= the_rank_of MVectors & (width A) -' (card N) >= the_rank_of MVectors ) by A26, A27, A36, A37, A33, A34, MATRIX13:74, MATRIX13:def 4;
hence the_rank_of MVectors = (width A) -' (card N) by XXREAL_0:1; :: thesis: verum

end;

then A38: lines MVectors is linearly-independent by MATRIX13:121;
reconsider B = lines MVectors as Subset of ((width A) -VectSp_over K) ;
MVectors is one-to-one by A35, MATRIX13:105;
then Seg ((width A) -' (card N)),B are_equipotent by A32, WELLORD2:def 4;
then card B = card (Seg ((width A) -' (card N))) by CARD_1:21
.= (width A) -' (card N) by FINSEQ_1:78 ;
hence dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A) by A31, A10, A27, A38, VECTSP_9:30; :: thesis: verum

end;

end;

end;

end;