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 ) ) )
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;
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 A5: 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
A6: i0 <> j0 and
A7: n0 <> m0 and
A8: [:{i0,j0},{n0,m0}:] c= Indices M ; :: thesis: Det (EqSegm (M,{i0,j0},{n0,m0})) = 0. K
A9: card {n0,m0} = 2 by A7, CARD_2:57;
assume A10: Det (EqSegm (M,{i0,j0},{n0,m0})) <> 0. K ; :: thesis: contradiction
card {i0,j0} = 2 by A6, CARD_2:57;
hence contradiction by A5, A8, A10, A9, 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 A11: the_rank_of M > 0 by Th94;
assume A12: 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 the_rank_of M <> 1 ; :: thesis: contradiction
then card P > 1 by A11, A3, NAT_1:25;
then card P >= 1 + 1 by NAT_1:13;
then consider P1 being finite Subset of P such that
A13: card P1 = 2 by FINSEQ_4:72;
not 0 in P1 ;
then reconsider P1 = P1 as finite without_zero Subset of NAT by MEASURE6:def 2, XBOOLE_1:1;
consider Q1 being finite without_zero Subset of NAT such that
A14: Q1 c= Q and
A15: card P1 = card Q1 and
A16: Det (EqSegm (M,P1,Q1)) <> 0. K by A2, A4, Th65;
consider n, m being object such that
A17: n <> m and
A18: Q1 = {n,m} by A13, A15, CARD_2:60;
A19: n in Q1 by A18, TARSKI:def 2;
m in Q1 by A18, TARSKI:def 2;
then reconsider n = n, m = m as non zero Element of NAT by A19;
consider i, j being object such that
A20: i <> j and
A21: P1 = {i,j} by A13, CARD_2:60;
A22: i in P1 by A21, TARSKI:def 2;
j in P1 by A21, TARSKI:def 2;
then reconsider i = i, j = j as non zero Element of NAT by A22;
[:P1,Q1:] c= [:P,Q:] by A14, ZFMISC_1:96;
then [:{i,j},{n,m}:] c= Indices M by A1, A21, A18;
hence contradiction by A12, A20, A21, A16, A17, A18; :: thesis: verum