let K be Field; :: thesis:
let M be Matrix of K; :: thesis:
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:

end;

assume ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) ; :: thesis:
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:
assume the_rank_of M <> 1 ; :: thesis:
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: