let K be Field; :: thesis: for M being Matrix of K holds
( the_rank_of M = 1 iff ( ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) & ( for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K ) ) )
let M be Matrix of K; :: thesis: ( the_rank_of M = 1 iff ( ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) & ( for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K ) ) )
thus ( the_rank_of M = 1 implies ( ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) & ( for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K ) ) ) :: thesis: ( ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) & ( for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K ) implies the_rank_of M = 1 )

proof

assume A1: the_rank_of M = 1 ; :: thesis: ( ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) & ( for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K ) )
hence ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) by Th94; :: thesis: for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K
let i0, j0, n0, m0 be non zero Nat; :: thesis: ( i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M implies Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K )
assume that
A2: ( i0 <> j0 & n0 <> m0 ) and
A3: [:{i0,j0},{n0,m0}:] c= Indices M ; :: thesis: Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K
assume A4: Det (EqSegm M,{i0,j0},{n0,m0}) <> 0. K ; :: thesis: contradiction
( card {i0,j0} = 2 & card {n0,m0} = 2 ) by A2, CARD_2:76;
hence contradiction by A1, A3, A4, Def4; :: thesis: verum

end;

assume ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) ; :: thesis: ( ex i0, j0, n0, m0 being non zero Nat st
( i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M & not Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K ) or the_rank_of M = 1 )
then A5: the_rank_of M > 0 by Th94;
assume A6: for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm M,{i0,j0},{n0,m0}) = 0. K ; :: thesis: the_rank_of M = 1
assume A7: the_rank_of M <> 1 ; :: thesis: contradiction
consider P, Q being finite without_zero Subset of NAT such that
A8: ( [:P,Q:] c= Indices M & card P = card Q ) and
A9: ( card P = the_rank_of M & Det (EqSegm M,P,Q) <> 0. K ) by Def4;
card P > 1 by A5, A7, A9, NAT_1:26;
then card P >= 1 + 1 by NAT_1:13;
then consider P1 being Subset of P such that
A10: card P1 = 2 by PENCIL_4:2;
not 0 in P1 ;
then reconsider P1 = P1 as finite without_zero Subset of NAT by PSCOMP_1:def 1, XBOOLE_1:1;
consider i, j being set such that
A11: ( i <> j & P1 = {i,j} ) by A10, CARD_2:79;
( i in P1 & j in P1 & not 0 in P1 ) by A11, TARSKI:def 2;
then reconsider i = i, j = j as non zero Element of NAT ;
consider Q1 being finite without_zero Subset of NAT such that
A12: ( Q1 c= Q & card P1 = card Q1 & Det (EqSegm M,P1,Q1) <> 0. K ) by A8, A9, Th65;
consider n, m being set such that
A13: ( n <> m & Q1 = {n,m} ) by A10, A12, CARD_2:79;
( n in Q1 & m in Q1 & not 0 in Q1 ) by A13, TARSKI:def 2;
then reconsider n = n, m = m as non zero Element of NAT ;
[:P1,Q1:] c= [:P,Q:] by A12, ZFMISC_1:119;
then [:{i,j},{n,m}:] c= Indices M by A8, A11, A13, XBOOLE_1:1;
hence contradiction by A6, A11, A12, A13; :: thesis: verum