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 ( {i,j} c= Seg (len M) & {n,p} c= Seg (width M) & i in {i,j} & j in {i,j} & p in {n,p} & n in {n,p} & not 0 in Seg (len M) & not 0 in Seg (width M) ) by A2, TARSKI:def 2, ZFMISC_1:138;
then reconsider I = i, J = j, P = p, N = n as non zero Element of NAT ;
A4: ( card {I,J} = 2 & card {N,P} = 2 ) by A3, CARD_2:76;
then A5: EqSegm M,{I,J},{N,P} = Segm M,{I,J},{N,P} by Def3;
A6: Det (EqSegm M,{I,J},{N,P}) = 0. K by A1, A2, A3, Th96;
set IN = M * I,N;
set IP = M * I,P;
set JN = M * J,N;
set JP = M * J,P;

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 A4, A5, A6, 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 A4, A5, A6, 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 A4, A5, A6, 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 A4, A5, A6, 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
A7: ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) and
A8: 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
A9: ( i0 <> j0 & n0 <> m0 ) and
A10: [:{i0,j0},{n0,m0}:] c= Indices M ; :: thesis: Det (EqSegm M,{b₁,b₂},{b₃,b₄}) = 0. K
A11: ( card {i0,j0} = 2 & card {n0,m0} = 2 ) by A9, CARD_2:76;
then A12: EqSegm M,{i0,j0},{n0,m0} = Segm M,{i0,j0},{n0,m0} by Def3;
set IN = M * i0,n0;
set IM = M * i0,m0;
set JN = M * j0,n0;
set JM = M * j0,m0;
A13: (M * i0,n0) * (M * j0,m0) = (M * i0,m0) * (M * j0,n0) by A8, A10;

per cases ( ( i0 < j0 & n0 < m0 ) or ( i0 < j0 & n0 > m0 ) or ( i0 > j0 & n0 < m0 ) or ( i0 > j0 & n0 > m0 ) ) by A9, 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 A12, Th45;
hence Det (EqSegm M,{i0,j0},{n0,m0}) = ((M * i0,n0) * (M * j0,m0)) - ((M * i0,m0) * (M * j0,n0)) by A11, MATRIX_9:13
.= 0. K by A13, 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 A12, Th45;
hence Det (EqSegm M,{i0,j0},{n0,m0}) = ((M * i0,m0) * (M * j0,n0)) - ((M * i0,n0) * (M * j0,m0)) by A11, MATRIX_9:13
.= 0. K by A13, 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 A12, Th45;
hence Det (EqSegm M,{i0,j0},{n0,m0}) = ((M * j0,n0) * (M * i0,m0)) - ((M * j0,m0) * (M * i0,n0)) by A11, MATRIX_9:13
.= 0. K by A13, 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 A12, Th45;
hence Det (EqSegm M,{i0,j0},{n0,m0}) = ((M * j0,m0) * (M * i0,n0)) - ((M * j0,n0) * (M * i0,m0)) by A11, MATRIX_9:13
.= 0. K by A13, VECTSP_1:66 ;
:: thesis: verum

end;

end;

end;

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