:: Basic Properties of the Rank of Matrices over a Field
:: by Karol P\c{a}k
::
:: Received August 28, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem Th1: :: MATRIX13:1
for D being non empty set
for n, m being Nat
for A being Matrix of n,m,D holds
( ( n = 0 implies m = 0 ) iff ( len A = n & width A = m ) )
proofend;

theorem Th2: :: MATRIX13:2
for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is Lower_Triangular_Matrix of n,K iff M @ is Upper_Triangular_Matrix of n,K )
proofend;

theorem Th3: :: MATRIX13:3
for n being Nat
for K being Field
for M being Matrix of n,K holds diagonal_of_Matrix M = diagonal_of_Matrix (M @)
proofend;

theorem Th4: :: MATRIX13:4
for n being Nat
for perm being Element of Permutations n st perm <> idseq n holds
( ex i being Nat st
( i in Seg n &amp; perm . i > i ) &amp; ex j being Nat st
( j in Seg n &amp; perm . j < j ) )
proofend;

theorem Th5: :: MATRIX13:5
for n being Nat
for K being Field
for M being Matrix of n,K
for perm being Element of Permutations n st perm <> idseq n &amp; ( M is Lower_Triangular_Matrix of n,K or M is Upper_Triangular_Matrix of n,K ) holds
(Path_product M) . perm = 0. K
proofend;

theorem Th6: :: MATRIX13:6
for n being Nat
for K being Field
for M being Matrix of n,K
for I being Element of Permutations n st I = idseq n holds
diagonal_of_Matrix M = Path_matrix (I,M)
proofend;

theorem Th7: :: MATRIX13:7
for n being Nat
for K being Field
for M being Upper_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)
proofend;

theorem Th8: :: MATRIX13:8
for n being Nat
for K being Field
for M being Lower_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)
proofend;

theorem Th9: :: MATRIX13:9
for X being finite set
for n being Nat holds card  {  Y where Y is Subset of X : card Y = n  }  = (card X) choose n
proofend;

theorem Th10: :: MATRIX13:10
for n being Nat holds card (2Set (Seg n)) = n choose 2
proofend;

theorem :: MATRIX13:11
for n being Nat
for R being Element of Permutations n st R = Rev (idseq n) holds
( R is even iff (n choose 2) mod 2 = 0 )
proofend;

theorem Th12: :: MATRIX13:12
for n being Nat
for K being Field
for M being Matrix of n,K
for R being Permutation of (Seg n) st R = Rev (idseq n) &amp; ( for i, j being Nat st i in Seg n &amp; j in Seg n &amp; i + j <= n holds
M * (i,j) = 0. K ) holds
M * R is Upper_Triangular_Matrix of n,K
proofend;

theorem Th13: :: MATRIX13:13
for n being Nat
for K being Field
for M being Matrix of n,K
for R being Permutation of (Seg n) st R = Rev (idseq n) &amp; ( for i, j being Nat st i in Seg n &amp; j in Seg n &amp; i + j > n + 1 holds
M * (i,j) = 0. K ) holds
M * R is Lower_Triangular_Matrix of n,K
proofend;

theorem :: MATRIX13:14
for n being Nat
for K being Field
for M being Matrix of n,K
for R being Element of Permutations n st R = Rev (idseq n) &amp; ( for i, j being Nat st i in Seg n &amp; j in Seg n &amp; i + j <= n holds
M * (i,j) = 0. K or for i, j being Nat st i in Seg n &amp; j in Seg n &amp; i + j > n + 1 holds
M * (i,j) = 0. K ) holds
Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)
proofend;

theorem Th15: :: MATRIX13:15
for n being Nat
for K being Field
for M being Matrix of n,K
for M1, M2 being Upper_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Upper_Triangular_Matrix of n,K &amp; diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) )
proofend;

theorem :: MATRIX13:16
for n being Nat
for K being Field
for M being Matrix of n,K
for M1, M2 being Lower_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Lower_Triangular_Matrix of n,K &amp; diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) )
proofend;

begin

definition
let D be non empty set ;
let M be Matrix of D;
let n, m be Nat;
let nt be Element of n -tuples_on NAT;
let mt be Element of m -tuples_on NAT;
func Segm (M,nt,mt) ->  Matrix of n,m,D means :Def1: :: MATRIX13:def 1
 for i, j being Nat st [i,j] in Indices it holds
it * (i,j) = M * ((nt . i),(mt . j));
existence
 ex b1 being Matrix of n,m,D st
for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = M * ((nt . i),(mt . j))
proofend;
uniqueness
 for b1, b2 being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = M * ((nt . i),(mt . j)) ) &amp; ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * (i,j) = M * ((nt . i),(mt . j)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Segm MATRIX13:def_1_:_
 for D being non empty set
for M being Matrix of D
for n, m being Nat
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for b7 being Matrix of n,m,D holds
( b7 = Segm (M,nt,mt) iff for i, j being Nat st [i,j] in Indices b7 holds
b7 * (i,j) = M * ((nt . i),(mt . j)) );

theorem Th17: :: MATRIX13:17
for D being non empty set
for n, m, i, j being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A )
proofend;

theorem Th18: :: MATRIX13:18
for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT holds
not ( [:(rng nt),(rng mt):] c= Indices A &amp; ( n = 0 implies m = 0 ) &amp; ( m = 0 implies n = 0 ) &amp; not (Segm (A,nt,mt)) @ = Segm ((A @),mt,nt) )
proofend;

theorem Th19: :: MATRIX13:19
for D being non empty set
for m, n being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A &amp; ( m = 0 implies n = 0 ) holds
Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @
proofend;

theorem Th20: :: MATRIX13:20
for D being non empty set
for A being Matrix of 1,D holds A = <*<*(A * (1,1))*>*>
proofend;

theorem Th21: :: MATRIX13:21
for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st n = 1 &amp; m = 1 holds
Segm (A,nt,mt) = <*<*(A * ((nt . 1),(mt . 1)))*>*>
proofend;

theorem Th22: :: MATRIX13:22
for D being non empty set
for A being Matrix of 2,D holds A = ((A * (1,1)),(A * (1,2))) ][ ((A * (2,1)),(A * (2,2)))
proofend;

theorem Th23: :: MATRIX13:23
for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st n = 2 &amp; m = 2 holds
Segm (A,nt,mt) = ((A * ((nt . 1),(mt . 1))),(A * ((nt . 1),(mt . 2)))) ][ ((A * ((nt . 2),(mt . 1))),(A * ((nt . 2),(mt . 2))))
proofend;

theorem Th24: :: MATRIX13:24
for D being non empty set
for m, i, n being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n &amp; rng mt c= Seg (width A) holds
Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt
proofend;

theorem Th25: :: MATRIX13:25
for D being non empty set
for m, i, n, j being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n &amp; j in Seg n &amp; nt . i = nt . j holds
Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)
proofend;

theorem Th26: :: MATRIX13:26
for i, n, j being Nat
for K being Field
for nt, nt1 being Element of n -tuples_on NAT
for M being Matrix of K st i in Seg n &amp; j in Seg n &amp; nt . i = nt . j &amp; i <> j holds
Det (Segm (M,nt,nt1)) = 0. K
proofend;

theorem Th27: :: MATRIX13:27
for n being Nat
for K being Field
for nt, nt1 being Element of n -tuples_on NAT
for M being Matrix of K st not nt is one-to-one holds
Det (Segm (M,nt,nt1)) = 0. K
proofend;

theorem Th28: :: MATRIX13:28
for D being non empty set
for n, j, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st j in Seg m &amp; rng nt c= Seg (len A) holds
Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt
proofend;

theorem Th29: :: MATRIX13:29
for D being non empty set
for n, i, m, j being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg m &amp; j in Seg m &amp; mt . i = mt . j holds
Col ((Segm (A,nt,mt)),i) = Col ((Segm (A,nt,mt)),j)
proofend;

theorem Th30: :: MATRIX13:30
for i, m, j being Nat
for K being Field
for mt, mt1 being Element of m -tuples_on NAT
for M being Matrix of K st i in Seg m &amp; j in Seg m &amp; mt . i = mt . j &amp; i <> j holds
Det (Segm (M,mt1,mt)) = 0. K
proofend;

theorem Th31: :: MATRIX13:31
for m being Nat
for K being Field
for mt, mt1 being Element of m -tuples_on NAT
for M being Matrix of K st not mt is one-to-one holds
Det (Segm (M,mt1,mt)) = 0. K
proofend;

theorem Th32: :: MATRIX13:32
for n being Nat
for nt, nt1 being Element of n -tuples_on NAT st nt is one-to-one &amp; nt1 is one-to-one &amp; rng nt = rng nt1 holds
ex perm being Permutation of (Seg n) st nt1 = nt * perm
proofend;

theorem Th33: :: MATRIX13:33
for D being non empty set
for m, n being Nat
for A being Matrix of D
for nt1, nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for f being Function of (Seg n),(Seg n) st nt1 = nt * f holds
Segm (A,nt1,mt) = (Segm (A,nt,mt)) * f
proofend;

theorem Th34: :: MATRIX13:34
for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt1, mt being Element of m -tuples_on NAT
for f being Function of (Seg m),(Seg m) st mt1 = mt * f holds
(Segm (A,nt,mt1)) @ = ((Segm (A,nt,mt)) @) * f
proofend;

theorem Th35: :: MATRIX13:35
for n being Nat
for K being Field
for nt1, nt2, nt being Element of n -tuples_on NAT
for M being Matrix of K
for perm being Element of Permutations n st nt1 = nt2 * perm holds
( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) &amp; Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) )
proofend;

Lm1:  for n being Nat
for nt, nt1 being Element of n -tuples_on NAT st rng nt = rng nt1 &amp; nt is one-to-one holds
nt1 is one-to-one
proofend;

theorem Th36: :: MATRIX13:36
for n being Nat
for K being Field
for M being Matrix of K
for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 &amp; rng nt1 = rng nt19 &amp; not Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) holds
Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19)))
proofend;

theorem Th37: :: MATRIX13:37
for D being non empty set
for n9, m9, n, m being Nat
for A9 being Matrix of n9,m9,D
for F, Fmt being FinSequence of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 &amp; Fmt = F * mt &amp; [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
proofend;

theorem Th38: :: MATRIX13:38
for D being non empty set
for n9, m9, m, n being Nat
for A9 being Matrix of n9,m9,D
for mt being Element of m -tuples_on NAT
for F being FinSequence of D
for i being Nat
for nt being Element of n -tuples_on NAT st not i in rng nt &amp; [:(rng nt),(rng mt):] c= Indices A9 holds
Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)
proofend;

theorem Th39: :: MATRIX13:39
for D being non empty set
for n9, m9, m, i, n, j being Nat
for A9 being Matrix of n9,m9,D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in rng nt &amp; [:(rng nt),(rng mt):] c= Indices A9 holds
ex nt1 being Element of n -tuples_on NAT st
( rng nt1 = ((rng nt) \ {i}) \/ {j} &amp; Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt) = Segm (A9,nt1,mt) )
proofend;

theorem Th40: :: MATRIX13:40
for D being non empty set
for n9, m9, i being Nat
for A9 being Matrix of n9,m9,D
for F being FinSequence of D st not i in Seg (len A9) holds
RLine (A9,i,F) = A9
proofend;

definition
let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let a be Element of K;
:: original:*
redefine funca * M ->  Matrix of n,m,K;
coherence
 a * M is Matrix of n,m,K
proofend;
end;

theorem Th41: :: MATRIX13:41
for n, m being Nat
for K being Field
for a being Element of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
a * (Segm (M,nt,mt)) = Segm ((a * M),nt,mt)
proofend;

theorem Th42: :: MATRIX13:42
for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st nt = idseq (len A) &amp; mt = idseq (width A) holds
Segm (A,nt,mt) = A
proofend;

registration
cluster empty finite without_zero for Element of bool NAT;
existence
 ex b1 being Subset of NAT st
( b1 is empty &amp; b1 is without_zero &amp; b1 is finite )
proofend;
cluster non empty finite without_zero for Element of bool NAT;
existence
 ex b1 being Subset of NAT st
( not b1 is empty &amp; b1 is without_zero &amp; b1 is finite )
proofend;
end;

registration
let n be Nat;
cluster Seg n ->  without_zero ;
coherence
 Seg n is without_zero
proofend;
end;

registration
let X be without_zero set ;
let Y be set ;
clusterX \ Y ->  without_zero ;
coherence
 X \ Y is without_zero
proofend;
end;

definition
let i be Nat;
:: original:{
redefine func{i} ->  Subset of NAT;
coherence
 {i} is Subset of NAT
proofend;
let j be Nat;
:: original:{
redefine func{i,j} ->  Subset of NAT;
coherence
 {i,j} is Subset of NAT
proofend;
end;

theorem Th43: :: MATRIX13:43
for N being finite without_zero Subset of NAT ex k being Nat st N c= Seg k
proofend;

definition
let N be finite without_zero Subset of NAT;
:: original:Sgm
redefine func Sgm N ->  Element of (card N) -tuples_on NAT;
coherence
 Sgm N is Element of (card N) -tuples_on NAT
proofend;
end;

definition
let D be non empty set ;
let A be Matrix of D;
let P, Q be finite without_zero Subset of NAT;
func Segm (A,P,Q) ->  Matrix of card P, card Q,D equals :: MATRIX13:def 2
 Segm (A,(Sgm P),(Sgm Q));
coherence
 Segm (A,(Sgm P),(Sgm Q)) is Matrix of card P, card Q,D ;
end;

:: deftheorem  defines Segm MATRIX13:def_2_:_
 for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT holds Segm (A,P,Q) = Segm (A,(Sgm P),(Sgm Q));

theorem Th44: :: MATRIX13:44
for D being non empty set
for i0, j0 being non zero Nat
for A being Matrix of D holds Segm (A,{i0},{j0}) = <*<*(A * (i0,j0))*>*>
proofend;

theorem Th45: :: MATRIX13:45
for D being non empty set
for i0, j0, n0, m0 being non zero Nat
for A being Matrix of D st i0 < j0 &amp; n0 < m0 holds
Segm (A,{i0,j0},{n0,m0}) = ((A * (i0,n0)),(A * (i0,m0))) ][ ((A * (j0,n0)),(A * (j0,m0)))
proofend;

theorem Th46: :: MATRIX13:46
for D being non empty set
for A being Matrix of D holds Segm (A,(Seg (len A)),(Seg (width A))) = A
proofend;

theorem Th47: :: MATRIX13:47
for D being non empty set
for i being Nat
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st i in Seg (card P) &amp; Q c= Seg (width A) holds
Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)
proofend;

theorem Th48: :: MATRIX13:48
for D being non empty set
for i being Nat
for A being Matrix of D
for P being finite without_zero Subset of NAT st i in Seg (card P) holds
Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i))
proofend;

theorem Th49: :: MATRIX13:49
for D being non empty set
for j being Nat
for A being Matrix of D
for Q, P being finite without_zero Subset of NAT st j in Seg (card Q) &amp; P c= Seg (len A) holds
Col ((Segm (A,P,Q)),j) = (Col (A,((Sgm Q) . j))) * (Sgm P)
proofend;

theorem Th50: :: MATRIX13:50
for D being non empty set
for j being Nat
for A being Matrix of D
for Q being finite without_zero Subset of NAT st j in Seg (card Q) holds
Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j))
proofend;

theorem Th51: :: MATRIX13:51
for D being non empty set
for i being Nat
for A being Matrix of D holds Segm (A,((Seg (len A)) \ {i}),(Seg (width A))) = Del (A,i)
proofend;

theorem Th52: :: MATRIX13:52
for i being Nat
for K being Field
for M being Matrix of K holds Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = DelCol (M,i)
proofend;

theorem Th53: :: MATRIX13:53
for X being set
for P being finite without_zero Subset of NAT holds (Sgm P) " X is finite without_zero Subset of NAT
proofend;

theorem Th54: :: MATRIX13:54
for X being set
for P being finite without_zero Subset of NAT st X c= P holds
Sgm X = (Sgm P) * (Sgm ((Sgm P) " X))
proofend;

Lm2:  for X being set
for P being finite without_zero Subset of NAT st X c= P holds
card X = card ((Sgm P) " X)
proofend;

theorem Th55: :: MATRIX13:55
for X, Y being set
for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT holds [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm (A,P,Q))
proofend;

theorem Th56: :: MATRIX13:56
for D being non empty set
for A being Matrix of D
for P, P1, Q, Q1, P2, Q2 being finite without_zero Subset of NAT st P c= P1 &amp; Q c= Q1 &amp; P2 = (Sgm P1) " P &amp; Q2 = (Sgm Q1) " Q holds
( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) &amp; Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )
proofend;

theorem Th57: :: MATRIX13:57
for D being non empty set
for A being Matrix of D
for P, Q, P1, Q1 being finite without_zero Subset of NAT holds
not ( ( P = {} implies Q = {} ) &amp; ( Q = {} implies P = {} ) &amp; [:P,Q:] c= Indices (Segm (A,P1,Q1)) &amp; ( for P2, Q2 being finite without_zero Subset of NAT holds
( not P2 c= P1 or not Q2 c= Q1 or not P2 = (Sgm P1) .: P or not Q2 = (Sgm Q1) .: Q or not card P2 = card P or not card Q2 = card Q or not Segm ((Segm (A,P1,Q1)),P,Q) = Segm (A,P2,Q2) ) ) )
proofend;

theorem Th58: :: MATRIX13:58
for n, i, j being Nat
for K being Field
for M being Matrix of n,K holds Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)
proofend;

theorem Th59: :: MATRIX13:59
for D being non empty set
for n9, m9, i being Nat
for A9 being Matrix of n9,m9,D
for Q, P being finite without_zero Subset of NAT
for F, FQ being FinSequence of D st len F = width A9 &amp; FQ = F * (Sgm Q) &amp; [:P,Q:] c= Indices A9 holds
RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)
proofend;

theorem Th60: :: MATRIX13:60
for D being non empty set
for n9, m9 being Nat
for A9 being Matrix of n9,m9,D
for Q being finite without_zero Subset of NAT
for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of NAT st not i in P &amp; [:P,Q:] c= Indices A9 holds
Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)
proofend;

theorem :: MATRIX13:61
for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT holds
not ( [:P,Q:] c= Indices A &amp; ( card P = 0 implies card Q = 0 ) &amp; ( card Q = 0 implies card P = 0 ) &amp; not (Segm (A,P,Q)) @ = Segm ((A @),Q,P) )
proofend;

theorem Th62: :: MATRIX13:62
for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A &amp; ( card Q = 0 implies card P = 0 ) holds
Segm (A,P,Q) = (Segm ((A @),Q,P)) @
proofend;

theorem Th63: :: MATRIX13:63
for K being Field
for a being Element of K
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds
a * (Segm (M,P,Q)) = Segm ((a * M),P,Q)
proofend;

definition
let D be non empty set ;
let A be Matrix of D;
let P, Q be finite without_zero Subset of NAT;
assume A1: card P = card Q ;
func EqSegm (A,P,Q) ->  Matrix of card P,D equals :Def3: :: MATRIX13:def 3
 Segm (A,P,Q);
coherence
 Segm (A,P,Q) is Matrix of card P,D by A1;
end;

:: deftheorem Def3 defines EqSegm MATRIX13:def_3_:_
 for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st card P = card Q holds
EqSegm (A,P,Q) = Segm (A,P,Q);

theorem Th64: :: MATRIX13:64
for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i, j being Nat st i in Seg (card P) &amp; j in Seg (card P) &amp; card P = card Q holds
( Delete ((EqSegm (M,P,Q)),i,j) = EqSegm (M,(P \ {((Sgm P) . i)}),(Q \ {((Sgm Q) . j)})) &amp; card (P \ {((Sgm P) . i)}) = card (Q \ {((Sgm Q) . j)}) )
proofend;

Lm3:  for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i being Nat st i in Seg (card P) &amp; Det (EqSegm (M,P,Q)) <> 0. K holds
ex j being Nat st
( j in Seg (card P) &amp; Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )
proofend;

theorem Th65: :: MATRIX13:65
for K being Field
for M being Matrix of K
for P, P1, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 &amp; P c= P1 &amp; Det (EqSegm (M,P1,Q1)) <> 0. K holds
ex Q being finite without_zero Subset of NAT st
( Q c= Q1 &amp; card P = card Q &amp; Det (EqSegm (M,P,Q)) <> 0. K )
proofend;

Lm4:  for j being Nat
for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i being Nat st j in Seg (card P) &amp; Det (EqSegm (M,P,Q)) <> 0. K holds
ex i being Nat st
( i in Seg (card P) &amp; Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )
proofend;

theorem :: MATRIX13:66
for K being Field
for M being Matrix of K
for P1, Q, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 &amp; Q c= Q1 &amp; Det (EqSegm (M,P1,Q1)) <> 0. K holds
ex P being finite without_zero Subset of NAT st
( P c= P1 &amp; card P = card Q &amp; Det (EqSegm (M,P,Q)) <> 0. K )
proofend;

theorem Th67: :: MATRIX13:67
for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st card P = card Q holds
( [:P,Q:] c= Indices A iff ( P c= Seg (len A) &amp; Q c= Seg (width A) ) )
proofend;

theorem Th68: :: MATRIX13:68
for m9, n9 being Nat
for K being Field
for M9 being Matrix of n9,m9,K
for P, Q being finite without_zero Subset of NAT
for i being Nat
for j0 being non zero Nat st j0 in Seg n9 &amp; i in P &amp; not j0 in P &amp; card P = card Q &amp; [:P,Q:] c= Indices M9 holds
( card P = card ((P \ {i}) \/ {j0}) &amp; [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 &amp; ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )
proofend;

theorem Th69: :: MATRIX13:69
for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st card P = card Q holds
( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @) )
proofend;

theorem Th70: :: MATRIX13:70
for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M &amp; card P = card Q holds
Det (EqSegm (M,P,Q)) = Det (EqSegm ((M @),Q,P))
proofend;

theorem Th71: :: MATRIX13:71
for n being Nat
for K being Field
for a being Element of K
for M being Matrix of n,K holds Det (a * M) = ((power K) . (a,n)) * (Det M)
proofend;

theorem Th72: :: MATRIX13:72
for K being Field
for a being Element of K
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M &amp; card P = card Q holds
Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q)))
proofend;

definition
let K be Field;
let M be Matrix of K;
func the_rank_of M ->  Element of NAT  means :Def4: :: MATRIX13:def 4
( ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M &amp; card P = card Q &amp; card P = it &amp; Det (EqSegm (M,P,Q)) <> 0. K ) &amp; ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M &amp; card P1 = card Q1 &amp; Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= it ) );
existence
 ex b1 being Element of NAT st
( ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M &amp; card P = card Q &amp; card P = b1 &amp; Det (EqSegm (M,P,Q)) <> 0. K ) &amp; ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M &amp; card P1 = card Q1 &amp; Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= b1 ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M &amp; card P = card Q &amp; card P = b1 &amp; Det (EqSegm (M,P,Q)) <> 0. K ) &amp; ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M &amp; card P1 = card Q1 &amp; Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= b1 ) &amp; ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M &amp; card P = card Q &amp; card P = b2 &amp; Det (EqSegm (M,P,Q)) <> 0. K ) &amp; ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M &amp; card P1 = card Q1 &amp; Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines the_rank_of MATRIX13:def_4_:_
 for K being Field
for M being Matrix of K
for b3 being Element of NAT holds
( b3 = the_rank_of M iff ( ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M &amp; card P = card Q &amp; card P = b3 &amp; Det (EqSegm (M,P,Q)) <> 0. K ) &amp; ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M &amp; card P1 = card Q1 &amp; Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= b3 ) ) );

theorem Th73: :: MATRIX13:73
for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M &amp; card P = card Q holds
( card P <= len M &amp; card Q <= width M )
proofend;

theorem Th74: :: MATRIX13:74
for K being Field
for M being Matrix of K holds
( the_rank_of M <= len M &amp; the_rank_of M <= width M )
proofend;

Lm5:  for n, m being Nat
for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K holds
not ( [:(rng nt),(rng mt):] c= Indices M &amp; ( n = 0 implies m = 0 ) &amp; ( m = 0 implies n = 0 ) &amp; ( for P1, P2 being finite without_zero Subset of NAT holds
( not P1 = rng nt or not P2 = rng mt ) ) )
proofend;

theorem Th75: :: MATRIX13:75
for n being Nat
for K being Field
for nt1, nt2 being Element of n -tuples_on NAT
for M being Matrix of K st [:(rng nt1),(rng nt2):] c= Indices M &amp; Det (Segm (M,nt1,nt2)) <> 0. K holds
ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt1 &amp; P2 = rng nt2 &amp; card P1 = card P2 &amp; card P1 = n &amp; Det (EqSegm (M,P1,P2)) <> 0. K )
proofend;

theorem Th76: :: MATRIX13:76
for K being Field
for M being Matrix of K
for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M &amp; Det (Segm (M,rt1,rt2)) <> 0. K ) &amp; ( for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M &amp; Det (Segm (M,nt1,nt2)) <> 0. K holds
n <= RANK ) ) )
proofend;

theorem Th77: :: MATRIX13:77
for n, m being Nat
for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st ( n = 0 or m = 0 ) holds
the_rank_of (Segm (M,nt,mt)) = 0
proofend;

theorem Th78: :: MATRIX13:78
for n, m being Nat
for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
the_rank_of M >= the_rank_of (Segm (M,nt,mt))
proofend;

theorem Th79: :: MATRIX13:79
for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds
the_rank_of M >= the_rank_of (Segm (M,P,Q))
proofend;

theorem Th80: :: MATRIX13:80
for K being Field
for M being Matrix of K
for P, P1, Q, Q1 being finite without_zero Subset of NAT st P c= P1 &amp; Q c= Q1 holds
the_rank_of (Segm (M,P,Q)) <= the_rank_of (Segm (M,P1,Q1))
proofend;

theorem Th81: :: MATRIX13:81
for f, g being Function st rng f c= rng g holds
ex h being Function st
( dom h = dom f &amp; rng h c= dom g &amp; f = g * h )
proofend;

theorem Th82: :: MATRIX13:82
for n, m being Nat
for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] = Indices M holds
the_rank_of M = the_rank_of (Segm (M,nt,mt))
proofend;

theorem Th83: :: MATRIX13:83
for n being Nat
for K being Field
for M being Matrix of n,K holds
( the_rank_of M = n iff Det M <> 0. K )
proofend;

theorem :: MATRIX13:84
for K being Field
for M being Matrix of K holds the_rank_of M = the_rank_of (M @)
proofend;

Lm6:  for n being Nat
for K being Field
for a being Element of K st a <> 0. K holds
(power K) . (a,n) <> 0. K
proofend;

theorem :: MATRIX13:85
for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for F being Permutation of (Seg n) holds the_rank_of M = the_rank_of (M * F)
proofend;

theorem :: MATRIX13:86
for K being Field
for a being Element of K
for M being Matrix of K st a <> 0. K holds
the_rank_of M = the_rank_of (a * M)
proofend;

theorem Th87: :: MATRIX13:87
for K being Field
for a being Element of K
for p, pf being FinSequence of K
for f being Function st pf = p * f &amp; rng f c= dom p holds
(a * p) * f = a * pf
proofend;

theorem Th88: :: MATRIX13:88
for K being Field
for p, pf, q, qf being FinSequence of K
for f being Function st pf = p * f &amp; rng f c= dom p &amp; qf = q * f &amp; rng f c= dom q holds
(p + q) * f = pf + qf
proofend;

theorem Th89: :: MATRIX13:89
for n9, m9, i being Nat
for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st a <> 0. K holds
the_rank_of M9 = the_rank_of (RLine (M9,i,(a * (Line (M9,i)))))
proofend;

theorem Th90: :: MATRIX13:90
for i being Nat
for K being Field
for M being Matrix of K st Line (M,i) = (width M) |-> (0. K) holds
the_rank_of (DelLine (M,i)) = the_rank_of M
proofend;

theorem Th91: :: MATRIX13:91
for n9, m9, i being Nat
for K being Field
for M9 being Matrix of n9,m9,K
for p being FinSequence of K st len p = width M9 holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))
proofend;

theorem Th92: :: MATRIX13:92
for n9, m9, j, i being Nat
for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) &amp; ( i = j implies a <> - (1_ K) ) holds
the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))
proofend;

theorem Th93: :: MATRIX13:93
for n9, m9, j, i being Nat
for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) &amp; j <> i holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))
proofend;

theorem Th94: :: MATRIX13:94
for K being Field
for M being Matrix of K holds
( the_rank_of M > 0 iff ex i, j being Nat st
( [i,j] in Indices M &amp; M * (i,j) <> 0. K ) )
proofend;

theorem :: MATRIX13:95
for K being Field
for M being Matrix of K holds
( the_rank_of M = 0 iff M = 0. (K,(len M),(width M)) )
proofend;

theorem Th96: :: MATRIX13:96
for K being Field
for M being Matrix of K holds
( the_rank_of M = 1 iff ( ex i, j being Nat st
( [i,j] in Indices M &amp; M * (i,j) <> 0. K ) &amp; ( for i0, j0, n0, m0 being non zero Nat st i0 <> j0 &amp; n0 <> m0 &amp; [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm (M,{i0,j0},{n0,m0})) = 0. K ) ) )
proofend;

theorem Th97: :: MATRIX13:97
for K being Field
for M being Matrix of K holds
( the_rank_of M = 1 iff ( ex i, j being Nat st
( [i,j] in Indices M &amp; M * (i,j) <> 0. K ) &amp; ( 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)) ) ) )
proofend;

theorem :: MATRIX13:98
for K being Field
for M being Matrix of K holds
( the_rank_of M = 1 iff ex i being Nat st
( i in Seg (len M) &amp; ex j being Nat st
( j in Seg (width M) &amp; M * (i,j) <> 0. K ) &amp; ( 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)) ) ) )
proofend;

registration
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular diagonal for FinSequence of the carrier of K * ;
existence
 ex b1 being Matrix of K st b1 is diagonal
proofend;
end;

theorem Th99: :: MATRIX13:99
for K being Field
for M being diagonal Matrix of K
for NonZero1 being set st NonZero1 =  {  i where i is Element of NAT : ( [i,i] in Indices M &amp; M * (i,i) <> 0. K )  }  holds
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M &amp; card P = card Q &amp; Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 &amp; Q c= NonZero1 )
proofend;

theorem Th100: :: MATRIX13:100
for K being Field
for M being diagonal Matrix of K
for P being finite without_zero Subset of NAT st [:P,P:] c= Indices M holds
Segm (M,P,P) is V162(b1)
proofend;

theorem :: MATRIX13:101
for K being Field
for M being diagonal Matrix of K
for NonZero1 being set st NonZero1 =  {  i where i is Element of NAT : ( [i,i] in Indices M &amp; M * (i,i) <> 0. K )  }  holds
the_rank_of M = card NonZero1
proofend;

theorem Th102: :: MATRIX13:102
for n being Nat
for K being Field
for a being Element of K
for v1, v2, v being Vector of (n -VectSp_over K)
for t1, t2, t being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K &amp; 0. (n -VectSp_over K) = n |-> (0. K) &amp; ( t1 = v1 &amp; t2 = v2 implies t1 + t2 = v1 + v2 ) &amp; ( t = v implies a * t = a * v ) )
proofend;

registration
let K be Field;
let n be Nat;
clustern -VectSp_over K ->  right_complementable Abelian add-associative right_zeroed ;
coherence
 ( n -VectSp_over K is right_complementable &amp; n -VectSp_over K is Abelian &amp; n -VectSp_over K is add-associative &amp; n -VectSp_over K is right_zeroed )
proofend;
end;

registration
let K be Field;
let n be Nat;
cluster  ->  Relation-like Function-like for Element of the carrier of (n -VectSp_over K);
correctness
coherence
for b1 being Vector of (n -VectSp_over K) holds
( b1 is Function-like &amp; b1 is Relation-like );
proofend;
end;

Lm7:  for m, n being Nat
for K being Field
for M being Matrix of m,n,K holds rng M is Subset of (n -VectSp_over K)
proofend;

notation
let K be Field;
let m, n be Nat;
let M be Matrix of m,n,K;
synonym  lines M for  rng K;
synonym  without_repeated_line M for  one-to-one ;
end;

definition
let K be Field;
let m, n be Nat;
let M be Matrix of m,n,K;
:: original:lines
redefine func lines M ->  Subset of (n -VectSp_over K);
coherence
 lines is Subset of (n -VectSp_over K) by Lm7;
end;

theorem Th103: :: MATRIX13:103
for x being set
for n, m being Nat
for K being Field
for M being Matrix of m,n,K holds
( x in lines M iff ex i being Nat st
( i in Seg m &amp; x = Line (M,i) ) )
proofend;

theorem :: MATRIX13:104
for n being Nat
for K being Field
for V being finite Subset of (n -VectSp_over K) ex M being Matrix of card V,n,K st
( M is without_repeated_line &amp; lines M = V )
proofend;

definition
let K be Field;
let n be Nat;
let F be FinSequence of (n -VectSp_over K);
func FinS2MX F ->  Matrix of len F,n,K equals :: MATRIX13:def 5
F;
coherence
 F is Matrix of len F,n,K
proofend;
end;

:: deftheorem  defines FinS2MX MATRIX13:def_5_:_
 for K being Field
for n being Nat
for F being FinSequence of (n -VectSp_over K) holds FinS2MX F = F;

definition
let K be Field;
let m, n be Nat;
let M be Matrix of m,n,K;
func MX2FinS M ->  FinSequence of (n -VectSp_over K) equals :: MATRIX13:def 6
M;
coherence
 M is FinSequence of (n -VectSp_over K)
proofend;
end;

:: deftheorem  defines MX2FinS MATRIX13:def_6_:_
 for K being Field
for m, n being Nat
for M being Matrix of m,n,K holds MX2FinS M = M;

theorem Th105: :: MATRIX13:105
for n, m being Nat
for K being Field
for M being Matrix of m,n,K st the_rank_of M = m holds
M is without_repeated_line
proofend;

theorem Th106: :: MATRIX13:106
for m, n, i being Nat
for K being Field
for a being Element of K
for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st i in Seg (len M) &amp; a = L . (M . i) holds
Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i))
proofend;

theorem Th107: :: MATRIX13:107
for m, i, n being Nat
for K being Field
for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st M is without_repeated_line &amp; Carrier L c= lines M &amp; i in Seg n holds
(Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))
proofend;

theorem Th108: :: MATRIX13:108
for n, m being Nat
for K being Field
for M, M1 being Matrix of m,n,K st M is without_repeated_line &amp; ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) holds
ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1
proofend;

theorem Th109: :: MATRIX13:109
for n, m being Nat
for K being Field
for M being Matrix of m,n,K st M is without_repeated_line holds
( ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) &amp; ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) &amp; ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) ) iff lines M is linearly-independent )
proofend;

theorem Th110: :: MATRIX13:110
for n, m being Nat
for K being Field
for M being Matrix of m,n,K st the_rank_of M = m holds
lines M is linearly-independent
proofend;

theorem Th111: :: MATRIX13:111
for n being Nat
for K being Field
for M being Diagonal of n,K st the_rank_of M = n holds
lines M is Basis of n -VectSp_over K
proofend;

Lm8:  for n being Nat
for K being Field holds
( lines (1. (K,n)) is Basis of n -VectSp_over K &amp; the_rank_of (1. (K,n)) = n )
proofend;

registration
let K be Field;
let n be Nat;
clustern -VectSp_over K ->  finite-dimensional ;
coherence
 n -VectSp_over K is finite-dimensional
proofend;
end;

theorem :: MATRIX13:112
for n being Nat
for K being Field holds dim (n -VectSp_over K) = n
proofend;

theorem Th113: :: MATRIX13:113
for n, m being Nat
for K being Field
for M being Matrix of m,n,K
for i being Nat
for a being Element of K st ( for j being Nat st j in Seg m holds
M * (j,i) = a ) holds
( M is without_repeated_line iff Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) is without_repeated_line )
proofend;

theorem Th114: :: MATRIX13:114
for n, m being Nat
for K being Field
for M being Matrix of m,n,K
for i being Nat st M is without_repeated_line &amp; lines M is linearly-independent &amp; ( for j being Nat st j in Seg m holds
M * (j,i) = 0. K ) holds
lines (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) is linearly-independent
proofend;

theorem Th115: :: MATRIX13:115
for K being Field
for a being Element of K
for V being VectSp of K
for U being finite Subset of V st U is linearly-independent holds
for u, v being Vector of V st u in U &amp; v in U &amp; u <> v holds
(U \ {u}) \/ {(u + (a * v))} is linearly-independent
proofend;

theorem Th116: :: MATRIX13:116
for x being set
for K being Field
for V being VectSp of K
for u, v being Vector of V holds
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )
proofend;

theorem Th117: :: MATRIX13:117
for n, m being Nat
for K being Field
for a being Element of K
for M being Matrix of m,n,K st lines M is linearly-independent &amp; M is without_repeated_line holds
for i, j being Nat st j in Seg (len M) &amp; i <> j holds
( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line &amp; lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )
proofend;

theorem Th118: :: MATRIX13:118
for m, n being Nat
for K being Field
for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m holds
lines (Segm (M,P,(Seg n))) c= lines M
proofend;

theorem Th119: :: MATRIX13:119
for m, n being Nat
for K being Field
for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m &amp; lines M is linearly-independent holds
lines (Segm (M,P,(Seg n))) is linearly-independent
proofend;

theorem Th120: :: MATRIX13:120
for m, n being Nat
for K being Field
for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m &amp; M is without_repeated_line holds
Segm (M,P,(Seg n)) is without_repeated_line
proofend;

theorem Th121: :: MATRIX13:121
for m, n being Nat
for K being Field
for M being Matrix of m,n,K holds
( ( lines M is linearly-independent &amp; M is without_repeated_line ) iff the_rank_of M = m )
proofend;

theorem Th122: :: MATRIX13:122
for n, m being Nat
for K being Field
for M being Matrix of m,n,K
for U being Subset of (n -VectSp_over K) st U c= lines M holds
ex P being finite without_zero Subset of NAT st
( P c= Seg m &amp; lines (Segm (M,P,(Seg n))) = U &amp; Segm (M,P,(Seg n)) is without_repeated_line )
proofend;

theorem :: MATRIX13:123
for m, n being Nat
for K being Field
for M being Matrix of m,n,K
for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent &amp; U c= lines M &amp; card U = RANK ) &amp; ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent &amp; W c= lines M holds
card W <= RANK ) ) )
proofend;