let K be Field; :: thesis: for M being Matrix of K holds
( the_rank_of M > 0 iff ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) )
let M be Matrix of K; :: thesis: ( the_rank_of M > 0 iff ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) )
set r = the_rank_of M;
thus ( the_rank_of M > 0 implies ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) ) :: thesis: ( ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) implies the_rank_of M > 0 )

proof

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;
assume the_rank_of M > 0 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K )
then consider x being set such that
A5: x in P by A3, CARD_1:47, XBOOLE_0:def 1;
reconsider x = x as non zero Element of NAT by A5;
{x} c= P by A5, ZFMISC_1:37;
then consider Q1 being finite without_zero Subset of NAT such that
A6: Q1 c= Q and
A7: card {x} = card Q1 and
A8: Det (EqSegm M,{x},Q1) <> 0. K by A2, A4, Th65;
consider y being set such that
A9: {y} = Q1 by A7, CARD_2:60;
y in {y} by TARSKI:def 1;
then reconsider y = y as non zero Element of NAT by A9;
take x ; :: thesis: ex j being Nat st
( [x,j] in Indices M & M * x,j <> 0. K )
take y ; :: thesis: ( [x,y] in Indices M & M * x,y <> 0. K )
y in Q1 by A9, TARSKI:def 1;
then [x,y] in [:P,Q:] by A5, A6, ZFMISC_1:106;
hence [x,y] in Indices M by A1; :: thesis: M * x,y <> 0. K
A10: card {x} = 1 by CARD_1:50;
EqSegm M,{x},Q1 = Segm M,{x},{y} by A7, A9, Def3
.= <*<*(M * x,y)*>*> by Th44 ;
hence M * x,y <> 0. K by A8, A10, MATRIX_3:36; :: thesis: verum

end;

given i, j being Nat such that A11: [i,j] in Indices M and
A12: M * i,j <> 0. K ; :: thesis: the_rank_of M > 0
A13: j in Seg (width M) by A11, ZFMISC_1:106;
Indices M = [:(Seg (len M)),(Seg (width M)):] by FINSEQ_1:def 3;
then A14: i in Seg (len M) by A11, ZFMISC_1:106;
then reconsider i = i, j = j as non zero Element of NAT by A13;
A15: card {i} = 1 by CARD_1:50;
A16: card {j} = 1 by CARD_1:50;
then EqSegm M,{i},{j} = Segm M,{i},{j} by Def3, CARD_1:50
.= <*<*(M * i,j)*>*> by Th44 ;
then A17: Det (EqSegm M,{i},{j}) <> 0. K by A12, A15, MATRIX_3:36;
A18: {j} c= Seg (width M) by A13, ZFMISC_1:37;
{i} c= Seg (len M) by A14, ZFMISC_1:37;
then [:{i},{j}:] c= Indices M by A15, A16, A18, Th67;
hence the_rank_of M > 0 by A15, A16, A17, Def4; :: thesis: verum