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 object such that
A5: x in P by A3, CARD_1:27, XBOOLE_0:def 1;
reconsider x = x as non zero Element of NAT by A5;
{x} c= P by A5, ZFMISC_1:31;
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 object such that
A9: {y} = Q1 by A7, CARD_2:42;
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:87;
hence [x,y] in Indices M by A1; :: thesis: M * (x,y) <> 0. K
A10: card {x} = 1 by CARD_1:30;
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:34; :: 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:87;
Indices M = [:(Seg (len M)),(Seg (width M)):] by FINSEQ_1:def 3;
then A14: i in Seg (len M) by A11, ZFMISC_1:87;
then reconsider i = i, j = j as non zero Element of NAT by A13;
A15: card {i} = 1 by CARD_1:30;
A16: card {j} = 1 by CARD_1:30;
then EqSegm (M,{i},{j}) = Segm (M,{i},{j}) by Def3, CARD_1:30
.= <*<*(M * (i,j))*>*> by Th44 ;
then A17: Det (EqSegm (M,{i},{j})) <> 0. K by A12, A15, MATRIX_3:34;
A18: {j} c= Seg (width M) by A13, ZFMISC_1:31;
{i} c= Seg (len M) by A14, ZFMISC_1:31;
then [:{i},{j}:] c= Indices M by A15, A16, A18, Th67;
hence the_rank_of M > 0 by A15, A16, A17, Def4; :: thesis: verum