let K be Field; :: thesis: for M being diagonal Matrix of K
for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds
the_rank_of M = card NonZero1
let M be diagonal Matrix of K; :: thesis: for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds
the_rank_of M = card NonZero1
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: ( 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 A5: 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
A6: NZ c= Seg (width M)

proof

let x be object ; :: 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 A5;
hence x in Seg (width M) by ZFMISC_1:87; :: thesis: verum

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

proof

let x be object ; :: 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 A5;
hence x in dom M by ZFMISC_1:87; :: thesis: verum

end;

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

now :: thesis: Det S <> 0. K

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 A8: card nz >= 1 ; :: thesis: Det S <> 0. K

set Sn = Sgm nz;

A9: now :: thesis: for k being Nat st k in dom (diagonal_of_Matrix S) holds
(diagonal_of_Matrix S) . k <> 0. K

A10: rng (Sgm nz) = nz by FINSEQ_1:def 14;
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: ( k in dom (diagonal_of_Matrix S) implies (diagonal_of_Matrix S) . k <> 0. K )
assume A13: k in dom (diagonal_of_Matrix S) ; :: thesis: (diagonal_of_Matrix S) . k <> 0. K
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 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: verum

end;

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

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