let K be Field; :: thesis: for M being Matrix of K holds
( the_rank_of M = 1 iff ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * i,j <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line M,k = a * (Line M,i) ) ) )
let M be Matrix of K; :: thesis: ( the_rank_of M = 1 iff ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * i,j <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line M,k = a * (Line M,i) ) ) )
A1: Indices M = [:(Seg (len M)),(Seg (width M)):] by FINSEQ_1:def 3;
thus ( the_rank_of M = 1 implies ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * i,j <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line M,k = a * (Line M,i) ) ) ) :: thesis: ( ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * i,j <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line M,k = a * (Line M,i) ) ) implies the_rank_of M = 1 )

proof

assume A2: the_rank_of M = 1 ; :: thesis: ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * i,j <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line M,k = a * (Line M,i) ) )
then consider i, j being Nat such that
A3: [i,j] in Indices M and
A4: M * i,j <> 0. K by Th97;
take i ; :: thesis: ( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * i,j <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line M,k = a * (Line M,i) ) )
A5: j in Seg (width M) by A3, ZFMISC_1:106;
hence ( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * i,j <> 0. K ) ) by A1, A3, A4, ZFMISC_1:106; :: thesis: for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line M,k = a * (Line M,i)
set Li = Line M,i;
set ij = M * i,j;
let k be Nat; :: thesis: ( k in Seg (len M) implies ex a being Element of K st Line M,k = a * (Line M,i) )
assume A6: k in Seg (len M) ; :: thesis: ex a being Element of K st Line M,k = a * (Line M,i)
set Lk = Line M,k;
set kj = M * k,j;
take a = (M * k,j) * ((M * i,j) " ); :: thesis: Line M,k = a * (Line M,i)
A7: i in Seg (len M) by A1, A3, ZFMISC_1:106;

A8: now

let n be Nat; :: thesis: ( 1 <= n & n <= width M implies (Line M,k) . n = (a * (Line M,i)) . n )
assume that
A9: 1 <= n and
A10: n <= width M ; :: thesis: (Line M,k) . n = (a * (Line M,i)) . n
n in NAT by ORDINAL1:def 13;
then A11: n in Seg (width M) by A9, A10;
then A12: {j,n} c= Seg (width M) by A5, ZFMISC_1:38;
(Line M,i) . n = M * i,n by A11, MATRIX_1:def 8;
then A13: (a * (Line M,i)) . n = a * (M * i,n) by A11, FVSUM_1:63;
A14: M * k,j = (M * k,j) * (1_ K) by VECTSP_1:def 13
.= (M * k,j) * ((M * i,j) * ((M * i,j) " )) by A4, VECTSP_1:def 22
.= a * (M * i,j) by GROUP_1:def 4 ;
{i,k} c= Seg (len M) by A7, A6, ZFMISC_1:38;
then [:{i,k},{j,n}:] c= Indices M by A1, A12, ZFMISC_1:119;
then A15: (M * i,j) * (M * k,n) = (a * (M * i,j)) * (M * i,n) by A2, A14, Th97
.= (M * i,j) * (a * (M * i,n)) by GROUP_1:def 4 ;
(Line M,k) . n = M * k,n by A11, MATRIX_1:def 8;
hence (Line M,k) . n = (a * (Line M,i)) . n by A4, A15, A13, VECTSP_2:42; :: thesis: verum

end;

A16: len (a * (Line M,i)) = width M by FINSEQ_1:def 18;
len (Line M,k) = width M by FINSEQ_1:def 18;
hence Line M,k = a * (Line M,i) by A16, A8, FINSEQ_1:18; :: thesis: verum

end;

given i being Nat such that A17: i in Seg (len M) and
A18: ex j being Nat st
( j in Seg (width M) & M * i,j <> 0. K ) and
A19: for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line M,k = a * (Line M,i) ; :: thesis: the_rank_of M = 1

A20: now

set Li = Line M,i;
let I, J, n, m be Nat; :: thesis: ( [:{I,J},{n,m}:] c= Indices M implies (M * I,n) * (M * J,m) = (M * I,m) * (M * J,n) )
assume A21: [:{I,J},{n,m}:] c= Indices M ; :: thesis: (M * I,n) * (M * J,m) = (M * I,m) * (M * J,n)
A22: {n,m} c= Seg (width M) by A21, ZFMISC_1:138;
then A23: n in Seg (width M) by ZFMISC_1:38;
then A24: (Line M,i) . n = M * i,n by MATRIX_1:def 8;
set LJ = Line M,J;
set LI = Line M,I;
A25: {I,J} c= Seg (len M) by A1, A21, ZFMISC_1:138;
then I in Seg (len M) by ZFMISC_1:38;
then consider a being Element of K such that
A26: Line M,I = a * (Line M,i) by A19;
J in Seg (len M) by A25, ZFMISC_1:38;
then consider b being Element of K such that
A27: Line M,J = b * (Line M,i) by A19;
(Line M,J) . n = M * J,n by A23, MATRIX_1:def 8;
then A28: M * J,n = b * (M * i,n) by A27, A23, A24, FVSUM_1:63;
A29: m in Seg (width M) by A22, ZFMISC_1:38;
then A30: (Line M,i) . m = M * i,m by MATRIX_1:def 8;
(Line M,J) . m = M * J,m by A29, MATRIX_1:def 8;
then A31: M * J,m = b * (M * i,m) by A27, A29, A30, FVSUM_1:63;
(Line M,I) . m = M * I,m by A29, MATRIX_1:def 8;
then A32: M * I,m = a * (M * i,m) by A26, A29, A30, FVSUM_1:63;
(Line M,I) . n = M * I,n by A23, MATRIX_1:def 8;
then M * I,n = a * (M * i,n) by A26, A23, A24, FVSUM_1:63;
hence (M * I,n) * (M * J,m) = ((a * (M * i,n)) * b) * (M * i,m) by A31, GROUP_1:def 4
.= ((b * (M * i,n)) * a) * (M * i,m) by GROUP_1:def 4
.= (M * I,m) * (M * J,n) by A28, A32, GROUP_1:def 4 ;
:: thesis: verum

end;

consider j being Nat such that
A33: j in Seg (width M) and
A34: M * i,j <> 0. K by A18;
[i,j] in Indices M by A1, A17, A33, ZFMISC_1:106;
hence the_rank_of M = 1 by A34, A20, Th97; :: thesis: verum