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

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

end;

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