let K be Field; :: thesis:
let M be diagonal Matrix of K; :: thesis:
consider P, Q being finite without_zero Subset of NAT such that
A1: [:P,Q:] c= Indices M and
A2: card P = card Q and
A3: card P = the_rank_of M and
A4: Det (EqSegm (M,P,Q)) <> 0. K by Def4;
let NZ be set ; :: thesis:
assume A5: NZ = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } ; :: thesis:
A6: NZ c= Seg (width M)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in NZ ; :: thesis:
then ex i being Element of NAT st
( x = i & [i,i] in Indices M & M * (i,i) <> 0. K ) by A5;
hence x in Seg (width M) by ZFMISC_1:87; :: thesis:

end;

then not 0 in NZ ;
then reconsider nz = NZ as finite without_zero Subset of NAT by A6, MEASURE6:def 2, XBOOLE_1:1;
set S = Segm (M,nz,nz);
NZ c= dom M

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in NZ ; :: thesis:
then ex i being Element of NAT st
( x = i & [i,i] in Indices M & M * (i,i) <> 0. K ) by A5;
hence x in dom M by ZFMISC_1:87; :: thesis:

end;

then A7: [:nz,nz:] c= Indices M by A6, ZFMISC_1:96;
then reconsider S = Segm (M,nz,nz) as V185(K) Matrix of card nz,K by Th100;
set d = diagonal_of_Matrix S;

per cases by NAT_1:14;

suppose card nz = 0 ; :: thesis:

then Det S = 1_ K by MATRIXR2:41;
hence Det S <> 0. K ; :: thesis:

end;

suppose A8: card nz >= 1 ; :: thesis:

set Sn = Sgm nz;

A9: now :: thesis:

A10: rng (Sgm nz) = nz by A6, FINSEQ_1:def 13;
A11: dom (diagonal_of_Matrix S) = Seg (len (diagonal_of_Matrix S)) by FINSEQ_1:def 3;
A12: len (diagonal_of_Matrix S) = card nz by MATRIX_3:def 10;
let k be Nat; :: thesis:
assume A13: k in dom (diagonal_of_Matrix S) ; :: thesis:
A14: (diagonal_of_Matrix S) . k = S * (k,k) by A13, A11, A12, MATRIX_3:def 10;
dom (Sgm nz) = dom (diagonal_of_Matrix S) by A6, A11, A12, FINSEQ_3:40;
then (Sgm nz) . k in nz by A13, A10, FUNCT_1:def 3;
then A15: ex i being Element of NAT st
( i = (Sgm nz) . k & [i,i] in Indices M & M * (i,i) <> 0. K ) by A5;
Indices S = [:(Seg (card nz)),(Seg (card nz)):] by MATRIX_0:24;
then [k,k] in Indices S by A13, A11, A12, ZFMISC_1:87;
hence (diagonal_of_Matrix S) . k <> 0. K by A14, A15, Def1; :: thesis:

end;

Det S = Product (diagonal_of_Matrix S) by A8, MATRIX_7:17;
hence Det S <> 0. K by A9, FVSUM_1:82; :: thesis:

end;

end;

end;

then Det (EqSegm (M,nz,nz)) <> 0. K by Def3;
then A16: the_rank_of M >= card nz by A7, Def4;
P c= nz by A5, A1, A2, A4, Th99;
then card P <= card nz by NAT_1:43;
hence the_rank_of M = card NZ by A16, A3, XXREAL_0:1; :: thesis: