let K be Field; :: thesis: for M being diagonal Matrix of K
for NonZero being set st NonZero = { i where i is Element of NAT : ( [i,i] in Indices M & M * i,i <> 0. K ) } holds
the_rank_of M = card NonZero
let M be diagonal Matrix of K; :: thesis: for NonZero being set st NonZero = { i where i is Element of NAT : ( [i,i] in Indices M & M * i,i <> 0. K ) } holds
the_rank_of M = card NonZero
let NZ be set ; :: thesis: ( NZ = { i where i is Element of NAT : ( [i,i] in Indices M & M * i,i <> 0. K ) } implies the_rank_of M = card NZ )
assume A1: NZ = { i where i is Element of NAT : ( [i,i] in Indices M & M * i,i <> 0. K ) } ; :: thesis: the_rank_of M = card NZ
A2: NZ c= Seg (width M)

proof

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

end;

A3: NZ c= dom M

proof

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

end;

( not 0 in NZ & NZ is finite ) by A2;
then reconsider nz = NZ as finite without_zero Subset of NAT by A2, PSCOMP_1:def 1, XBOOLE_1:1;
set S = Segm M,nz,nz;
A4: [:nz,nz:] c= Indices M by A2, A3, ZFMISC_1:119;
then reconsider S = Segm M,nz,nz as V146(K) Matrix of card nz,K by Th100;
set d = diagonal_of_Matrix S;

now

per cases ( card nz = 0 or card nz >= 1 ) by NAT_1:14;

suppose card nz = 0 ; :: thesis: Det S <> 0. K

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

end;

suppose card nz >= 1 ; :: thesis: Det S <> 0. K

then A5: Det S = Product (diagonal_of_Matrix S) by MATRIX_7:17;
set Sn = Sgm nz;

now

let k be Element of NAT ; :: thesis: ( k in dom (diagonal_of_Matrix S) implies (diagonal_of_Matrix S) . k <> 0. K )
assume A6: k in dom (diagonal_of_Matrix S) ; :: thesis: (diagonal_of_Matrix S) . k <> 0. K
( dom (diagonal_of_Matrix S) = Seg (len (diagonal_of_Matrix S)) & len (diagonal_of_Matrix S) = card nz & Indices S = [:(Seg (card nz)),(Seg (card nz)):] ) by FINSEQ_1:def 3, MATRIX_1:25, MATRIX_3:def 10;
then A7: ( (diagonal_of_Matrix S) . k = S * k,k & [k,k] in Indices S & rng (Sgm nz) = nz & dom (Sgm nz) = dom (diagonal_of_Matrix S) ) by A2, A6, FINSEQ_1:def 13, FINSEQ_3:45, MATRIX_3:def 10, ZFMISC_1:106;
then (Sgm nz) . k in nz by A6, FUNCT_1:def 5;
then ex i being Element of NAT st
( i = (Sgm nz) . k & [i,i] in Indices M & M * i,i <> 0. K ) by A1;
hence (diagonal_of_Matrix S) . k <> 0. K by A7, Def1; :: thesis: verum

end;

hence Det S <> 0. K by A5, FVSUM_1:107; :: thesis: verum

end;

end;

end;

then Det (EqSegm M,nz,nz) <> 0. K by Def3;
then A8: the_rank_of M >= card nz by A4, Def4;
consider P, Q being finite without_zero Subset of NAT such that
A9: ( [:P,Q:] c= Indices M & card P = card Q ) and
A10: ( card P = the_rank_of M & Det (EqSegm M,P,Q) <> 0. K ) by Def4;
P c= nz by A1, A9, A10, Th99;
then card P <= card nz by NAT_1:44;
hence the_rank_of M = card NZ by A8, A10, XXREAL_0:1; :: thesis: verum