let K be Field; :: thesis: for A being Matrix of K st ( width A = 0 implies len A = 0 ) holds
dim = () - ()

let A be Matrix of K; :: thesis: ( ( width A = 0 implies len A = 0 ) implies dim = () - () )
assume A1: ( width A = 0 implies len A = 0 ) ; :: thesis: dim = () - ()
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 = () - ()
dim (() -VectSp_over K) = width A by MATRIX13:112;
hence dim = () - () by A1, A2, Th63; :: thesis: verum
end;
suppose A3: the_rank_of A > 0 ; :: thesis: dim = () - ()
defpred S1[ 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 H1( 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 ;
A5: for A1, B1 being Matrix of len A, width A,K st S1[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
S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]
proof
let A1, B1 be Matrix of len A, width A,K; :: thesis: ( S1[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
S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)] )

assume A6: S1[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
S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(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
S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]

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: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) implies S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)] )
assume ( j in dom A1 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]
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 S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)] ; :: thesis: verum
end;
A8: S1[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 () and
A10: ( the_rank_of A9 = the_rank_of A1 & the_rank_of A9 = card N ) and
A11: ( S1[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) = () |-> (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 A13: 0 < len A by ;
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 ()) \ N) = () - (card N) by ;
set SN = Segm (A1,(Seg (card N)),(Seg (width A1)));
A17: Seg (card N) c= Seg (card N) ;
A18: (width A) -' (card N) = () - (card N) by ;
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 ;
Sgm (Seg (width A1)) = idseq (width A1) by FINSEQ_3:48
.= id (Seg (width A1)) ;
then N = (Sgm (Seg (width A1))) " N by ;
then A20: Segm ((Segm (A1,(Seg (card N)),(Seg (width A1)))),(Seg (card N)),N) = 1. (K,(card N)) by ;
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: for i being Nat st i in (dom A1) \ (Seg (card N)) holds
Line (A1,i) = (width A1) |-> (0. K)
let i be Nat; :: thesis: ( i in (dom A1) \ (Seg (card N)) implies Line (A1,i) = (width A1) |-> (0. K) )
assume A24: i in (dom A1) \ (Seg (card N)) ; :: thesis: Line (A1,i) = (width A1) |-> (0. K)
not i in Seg (card N) by ;
then A25: ( i < 1 or i > card N ) ;
i in dom A1 by ;
hence Line (A1,i) = (width A1) |-> (0. K) by ; :: thesis: verum
end;
card N <= len A1 by ;
then A26: Seg (card N) c= Seg (len A1) by FINSEQ_1:5;
width A1 > 0 by ;
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 () -' (card N) > 0 ) ;
suppose A28: (width A) -' (card N) = 0 ; :: thesis: dim = () - ()
then Segm (A1,(Seg (card N)),(Seg (width A1))) = 1. (K,(card N)) by ;
hence dim = () - () by A10, A27, A18, A28, Lm8; :: thesis: verum
end;
suppose A29: (width A) -' (card N) > 0 ; :: thesis: dim = () - ()
then ((width A) -' (card N)) + 0 > 0 ;
then (width A) -' (card N) >= 1 by NAT_1:19;
then A30: Det (1. (K,(() -' (card N)))) = 1_ K by MATRIX_7:16;
A31: ( card (Seg (() -' (card N))) = () -' (card N) & 0. K <> 1_ K ) by FINSEQ_1:57;
consider MVectors being Matrix of () -' (card N), width A,K such that
A32: Segm (MVectors,(Seg (() -' (card N))),((Seg ()) \ N)) = 1. (K,(() -' (card N))) and
Segm (MVectors,(Seg (() -' (card N))),N) = - ((Segm ((Segm (A1,(Seg (card N)),(Seg (width A1)))),(Seg (card N)),((Seg ()) \ N))) @) and
A33: Lin (lines MVectors) = Space_of_Solutions_of A9 by A3, A9, A10, A27, A21, A15, A20, A29, Th67;
len MVectors = () -' (card N) by ;
then A34: (width A) -' (card N) >= the_rank_of MVectors by MATRIX13:74;
A35: (Seg ()) \ N c= Seg () by XBOOLE_1:36;
Indices MVectors = [:(Seg (() -' (card N))),(Seg ()):] by ;
then A36: [:(Seg (() -' (card N))),((Seg ()) \ N):] c= Indices MVectors by ;
reconsider B = lines MVectors as Subset of (() -VectSp_over K) ;
A37: ( dom MVectors = Seg (len MVectors) & len MVectors = () -' (card N) ) by ;
EqSegm (MVectors,(Seg (() -' (card N))),((Seg ()) \ N)) = 1. (K,(() -' (card N))) by ;
then A38: (width A) -' (card N) <= the_rank_of MVectors by ;
then MVectors is without_repeated_line by ;
then Seg (() -' (card N)),B are_equipotent by ;
then A39: card B = card (Seg (() -' (card N))) by CARD_1:5
.= () -' (card N) by FINSEQ_1:57 ;
the_rank_of MVectors = () -' (card N) by ;
then lines MVectors is linearly-independent by MATRIX13:121;
hence dim = () - () by ; :: thesis: verum
end;
end;
end;
end;