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 i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * i,n) * (M * j,m) = (M * i,m) * (M * j,n) ) ) )
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 i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * i,n) * (M * j,m) = (M * i,m) * (M * j,n) ) ) )
thus ( the_rank_of M = 1 implies ( ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * i,n) * (M * j,m) = (M * i,m) * (M * j,n) ) ) ) :: thesis: ( ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * i,n) * (M * j,m) = (M * i,m) * (M * j,n) ) 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 i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * i,n) * (M * j,m) = (M * i,m) * (M * j,n) ) )
hence ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) by Th96; :: thesis: for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * i,n) * (M * j,m) = (M * i,m) * (M * j,n)
let i, j, n, p be Nat; :: thesis: ( [:{i,j},{n,p}:] c= Indices M implies (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n) )
assume A2: [:{i,j},{n,p}:] c= Indices M ; :: thesis: (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n)

per cases ( i = j or n = p or ( i <> j & n <> p ) ) ;

suppose ( i = j or n = p ) ; :: thesis: (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n)

hence (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n) ; :: thesis: verum

end;

suppose A3: ( i <> j & n <> p ) ; :: thesis: (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n)

Indices M = [:(Seg (len M)),(Seg (width M)):] by FINSEQ_1:def 3;
then A4: {i,j} c= Seg (len M) by A2, ZFMISC_1:138;
A5: i in {i,j} by TARSKI:def 2;
A6: n in {n,p} by TARSKI:def 2;
A7: p in {n,p} by TARSKI:def 2;
A8: j in {i,j} by TARSKI:def 2;
{n,p} c= Seg (width M) by A2, ZFMISC_1:138;
then reconsider I = i, J = j, P = p, N = n as non zero Element of NAT by A4, A5, A8, A7, A6;
A9: card {I,J} = 2 by A3, CARD_2:76;
set JP = M * J,P;
set JN = M * J,N;
set IP = M * I,P;
set IN = M * I,N;
A10: Det (EqSegm M,{I,J},{N,P}) = 0. K by A1, A2, A3, Th96;
card {N,P} = 2 by A3, CARD_2:76;
then A11: EqSegm M,{I,J},{N,P} = Segm M,{I,J},{N,P} by A9, Def3;

per cases ( ( I < J & N < P ) or ( I < J & N > P ) or ( I > J & N < P ) or ( I > J & N > P ) ) by A3, XXREAL_0:1;

suppose ( I < J & N < P ) ; :: thesis: (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n)

then 0. K = Det ((M * I,N),(M * I,P) ][ (M * J,N),(M * J,P)) by A9, A11, A10, Th45
.= ((M * I,N) * (M * J,P)) - ((M * I,P) * (M * J,N)) by MATRIX_9:13 ;
hence (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n) by VECTSP_1:66; :: thesis: verum

end;

suppose ( I < J & N > P ) ; :: thesis: (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n)

then 0. K = Det ((M * I,P),(M * I,N) ][ (M * J,P),(M * J,N)) by A9, A11, A10, Th45
.= ((M * I,P) * (M * J,N)) - ((M * I,N) * (M * J,P)) by MATRIX_9:13 ;
hence (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n) by VECTSP_1:66; :: thesis: verum

end;

suppose ( I > J & N < P ) ; :: thesis: (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n)

then 0. K = Det ((M * J,N),(M * J,P) ][ (M * I,N),(M * I,P)) by A9, A11, A10, Th45
.= ((M * J,N) * (M * I,P)) - ((M * J,P) * (M * I,N)) by MATRIX_9:13 ;
hence (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n) by VECTSP_1:66; :: thesis: verum

end;

suppose ( I > J & N > P ) ; :: thesis: (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n)

then 0. K = Det ((M * J,P),(M * J,N) ][ (M * I,P),(M * I,N)) by A9, A11, A10, Th45
.= ((M * J,P) * (M * I,N)) - ((M * J,N) * (M * I,P)) by MATRIX_9:13 ;
hence (M * i,n) * (M * j,p) = (M * i,p) * (M * j,n) by VECTSP_1:66; :: thesis: verum

end;

end;

end;

end;

end;

assume that
A12: ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) and
A13: for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * i,n) * (M * j,m) = (M * i,m) * (M * j,n) ; :: thesis: the_rank_of M = 1

now

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,{b₁,b₂},{b₃,b₄}) = 0. K )
assume that
A14: i0 <> j0 and
A15: n0 <> m0 and
A16: [:{i0,j0},{n0,m0}:] c= Indices M ; :: thesis: Det (EqSegm M,{b₁,b₂},{b₃,b₄}) = 0. K
A17: card {i0,j0} = 2 by A14, CARD_2:76;
set JM = M * j0,m0;
set JN = M * j0,n0;
set IM = M * i0,m0;
set IN = M * i0,n0;
A18: (M * i0,n0) * (M * j0,m0) = (M * i0,m0) * (M * j0,n0) by A13, A16;
card {n0,m0} = 2 by A15, CARD_2:76;
then A19: EqSegm M,{i0,j0},{n0,m0} = Segm M,{i0,j0},{n0,m0} by A17, Def3;

per cases ( ( i0 < j0 & n0 < m0 ) or ( i0 < j0 & n0 > m0 ) or ( i0 > j0 & n0 < m0 ) or ( i0 > j0 & n0 > m0 ) ) by A14, A15, XXREAL_0:1;

suppose ( i0 < j0 & n0 < m0 ) ; :: thesis: Det (EqSegm M,{b₁,b₂},{b₃,b₄}) = 0. K

then EqSegm M,{i0,j0},{n0,m0} = (M * i0,n0),(M * i0,m0) ][ (M * j0,n0),(M * j0,m0) by A19, Th45;
hence Det (EqSegm M,{i0,j0},{n0,m0}) = ((M * i0,n0) * (M * j0,m0)) - ((M * i0,m0) * (M * j0,n0)) by A17, MATRIX_9:13
.= 0. K by A18, VECTSP_1:66 ;
:: thesis: verum

end;

suppose ( i0 < j0 & n0 > m0 ) ; :: thesis: Det (EqSegm M,{b₁,b₂},{b₃,b₄}) = 0. K

then EqSegm M,{i0,j0},{n0,m0} = (M * i0,m0),(M * i0,n0) ][ (M * j0,m0),(M * j0,n0) by A19, Th45;
hence Det (EqSegm M,{i0,j0},{n0,m0}) = ((M * i0,m0) * (M * j0,n0)) - ((M * i0,n0) * (M * j0,m0)) by A17, MATRIX_9:13
.= 0. K by A18, VECTSP_1:66 ;
:: thesis: verum

end;

suppose ( i0 > j0 & n0 < m0 ) ; :: thesis: Det (EqSegm M,{b₁,b₂},{b₃,b₄}) = 0. K

then EqSegm M,{i0,j0},{n0,m0} = (M * j0,n0),(M * j0,m0) ][ (M * i0,n0),(M * i0,m0) by A19, Th45;
hence Det (EqSegm M,{i0,j0},{n0,m0}) = ((M * j0,n0) * (M * i0,m0)) - ((M * j0,m0) * (M * i0,n0)) by A17, MATRIX_9:13
.= 0. K by A18, VECTSP_1:66 ;
:: thesis: verum

end;

suppose ( i0 > j0 & n0 > m0 ) ; :: thesis: Det (EqSegm M,{b₁,b₂},{b₃,b₄}) = 0. K

then EqSegm M,{i0,j0},{n0,m0} = (M * j0,m0),(M * j0,n0) ][ (M * i0,m0),(M * i0,n0) by A19, Th45;
hence Det (EqSegm M,{i0,j0},{n0,m0}) = ((M * j0,m0) * (M * i0,n0)) - ((M * j0,n0) * (M * i0,m0)) by A17, MATRIX_9:13
.= 0. K by A18, VECTSP_1:66 ;
:: thesis: verum

end;

end;

end;

hence the_rank_of M = 1 by A12, Th96; :: thesis: verum