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:87;
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:87; :: 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:87;

A8: now :: thesis: for n being Nat st 1 <= n & n <= width M holds
(Line (M,k)) . n = (a * (Line (M,i))) . n

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
A11: n in Seg (width M) by A9, A10;
then A12: {j,n} c= Seg (width M) by A5, ZFMISC_1:32;
(Line (M,i)) . n = M * (i,n) by A11, MATRIX_0:def 7;
then A13: (a * (Line (M,i))) . n = a * (M * (i,n)) by A11, FVSUM_1:51;
A14: M * (k,j) = (M * (k,j)) * (1_ K)
.= (M * (k,j)) * ((M * (i,j)) * ((M * (i,j)) ")) by A4, VECTSP_1:def 10
.= a * (M * (i,j)) by GROUP_1:def 3 ;
{i,k} c= Seg (len M) by A7, A6, ZFMISC_1:32;
then [:{i,k},{j,n}:] c= Indices M by A1, A12, ZFMISC_1:96;
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 3 ;
(Line (M,k)) . n = M * (k,n) by A11, MATRIX_0:def 7;
hence (Line (M,k)) . n = (a * (Line (M,i))) . n by A4, A15, A13, VECTSP_2:8; :: thesis: verum

end;

A16: len (a * (Line (M,i))) = width M by CARD_1:def 7;
len (Line (M,k)) = width M by CARD_1:def 7;
hence Line (M,k) = a * (Line (M,i)) by A16, A8; :: 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 :: 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))

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:114;
then A23: n in Seg (width M) by ZFMISC_1:32;
then A24: (Line (M,i)) . n = M * (i,n) by MATRIX_0:def 7;
set LJ = Line (M,J);
set LI = Line (M,I);
A25: {I,J} c= Seg (len M) by A1, A21, ZFMISC_1:114;
then I in Seg (len M) by ZFMISC_1:32;
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:32;
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_0:def 7;
then A28: M * (J,n) = b * (M * (i,n)) by A27, A23, A24, FVSUM_1:51;
A29: m in Seg (width M) by A22, ZFMISC_1:32;
then A30: (Line (M,i)) . m = M * (i,m) by MATRIX_0:def 7;
(Line (M,J)) . m = M * (J,m) by A29, MATRIX_0:def 7;
then A31: M * (J,m) = b * (M * (i,m)) by A27, A29, A30, FVSUM_1:51;
(Line (M,I)) . m = M * (I,m) by A29, MATRIX_0:def 7;
then A32: M * (I,m) = a * (M * (i,m)) by A26, A29, A30, FVSUM_1:51;
(Line (M,I)) . n = M * (I,n) by A23, MATRIX_0:def 7;
then M * (I,n) = a * (M * (i,n)) by A26, A23, A24, FVSUM_1:51;
hence (M * (I,n)) * (M * (J,m)) = ((a * (M * (i,n))) * b) * (M * (i,m)) by A31, GROUP_1:def 3
.= ((b * (M * (i,n))) * a) * (M * (i,m)) by GROUP_1:def 3
.= (M * (I,m)) * (M * (J,n)) by A28, A32, GROUP_1:def 3 ;
:: 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:87;
hence the_rank_of M = 1 by A34, A20, Th97; :: thesis: verum