let m, n be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
let K be Field; :: thesis: for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
defpred S₁[ Nat] means for m, n being Nat st m = $1 holds
for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
let m, n be Nat; :: thesis: ( m = k + 1 implies for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m ) )
assume A3: m = k + 1 ; :: thesis: for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
let M be Matrix of m,n,K; :: thesis: ( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
thus ( lines M is linearly-independent & M is without_repeated_line implies the_rank_of M = m ) :: thesis: ( the_rank_of M = m implies ( lines M is linearly-independent & M is without_repeated_line ) )

proof

A4: k < m by A3, NAT_1:13;
A5: len (n |-> (0. K)) = n by FINSEQ_1:def 18;
k < m by A3, NAT_1:13;
then A6: Seg k c= Seg m by FINSEQ_1:7;
A7: m in Seg m by A3, FINSEQ_1:6;
then Line M,m in lines M by Th103;
then reconsider LM = Line M,m as Element of n -tuples_on the carrier of K by Th102;
A8: len LM = n by FINSEQ_1:def 18;
assume that
A9: lines M is linearly-independent and
A10: M is without_repeated_line ; :: thesis: the_rank_of M = m
LM <> n |-> (0. K) by A9, A10, A7, Th109;
then consider i being Nat such that
A11: 1 <= i and
A12: i <= n and
A13: LM . i <> (n |-> (0. K)) . i by A8, A5, FINSEQ_1:18;
defpred S₂[ Nat] means ( $1 < m implies ex M1 being Matrix of m,n,K st
( Line M1,m = Line M,m & lines M1 is linearly-independent & M1 is without_repeated_line & the_rank_of M1 = the_rank_of M & ( for j being Nat st j <= $1 & j in Seg m holds
M1 * j,i = 0. K ) ) );
i in NAT by ORDINAL1:def 13;
then A14: i in Seg n by A11, A12;
then A15: LM . i <> 0. K by A13, FINSEQ_2:71;
len (Line M,m) = width M by MATRIX_1:def 8;
then A16: LM . i = M * m,i by A8, A14, MATRIX_1:def 8;
A17: for l being Nat st S₂[l] holds
S₂[l + 1]

proof

set Mmi = M * m,i;
let L be Nat; :: thesis: ( S₂[L] implies S₂[L + 1] )
assume A18: S₂[L] ; :: thesis: S₂[L + 1]
set L1 = L + 1;
assume A19: L + 1 < m ; :: thesis: ex M1 being Matrix of m,n,K st
( Line M1,m = Line M,m & lines M1 is linearly-independent & M1 is without_repeated_line & the_rank_of M1 = the_rank_of M & ( for j being Nat st j <= L + 1 & j in Seg m holds
M1 * j,i = 0. K ) )
then consider M1 being Matrix of m,n,K such that
A20: Line M1,m = Line M,m and
A21: lines M1 is linearly-independent and
A22: M1 is without_repeated_line and
A23: the_rank_of M1 = the_rank_of M and
A24: for j being Nat st j <= L & j in Seg m holds
M1 * j,i = 0. K by A18, NAT_1:13;
set MLi = M1 * (L + 1),i;
take R = RLine M1,(L + 1),((Line M1,(L + 1)) + ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (Line M1,m))); :: thesis: ( Line R,m = Line M,m & lines R is linearly-independent & R is without_repeated_line & the_rank_of R = the_rank_of M & ( for j being Nat st j <= L + 1 & j in Seg m holds
R * j,i = 0. K ) )
len M1 = m by MATRIX_1:def 3;
hence ( Line R,m = Line M,m & lines R is linearly-independent & R is without_repeated_line & the_rank_of R = the_rank_of M ) by A7, A19, A20, A21, A22, A23, Th92, Th117, MATRIX11:28; :: thesis: for j being Nat st j <= L + 1 & j in Seg m holds
R * j,i = 0. K
set LMm = Line M1,m;
set LML = Line M1,(L + 1);
let j be Nat; :: thesis: ( j <= L + 1 & j in Seg m implies R * j,i = 0. K )
assume that
A25: j <= L + 1 and
A26: j in Seg m ; :: thesis: R * j,i = 0. K
m <> 0 by A26;
then A27: width M1 = n by Th1;
then A28: (Line M1,(L + 1)) . i = M1 * (L + 1),i by A14, MATRIX_1:def 8;
0 + 1 <= L + 1 by NAT_1:13;
then A29: L + 1 in Seg m by A19;
len ((Line M1,(L + 1)) + ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (Line M1,m))) = width M1 by FINSEQ_1:def 18;
then A30: Line R,(L + 1) = (Line M1,(L + 1)) + ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (Line M1,m)) by A29, MATRIX11:28;
m <> 0 by A26;
then width M = n by Th1;
then (Line M1,m) . i = M * m,i by A14, A20, MATRIX_1:def 8;
then ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (Line M1,m)) . i = (- (((M * m,i) " ) * (M1 * (L + 1),i))) * (M * m,i) by A14, A27, FVSUM_1:63;
then A31: (Line R,(L + 1)) . i = (M1 * (L + 1),i) + ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (M * m,i)) by A14, A27, A28, A30, FVSUM_1:22
.= (M1 * (L + 1),i) + ((- ((1_ K) * (((M * m,i) " ) * (M1 * (L + 1),i)))) * (M * m,i)) by VECTSP_1:def 13
.= (M1 * (L + 1),i) + (((- (1_ K)) * (((M * m,i) " ) * (M1 * (L + 1),i))) * (M * m,i)) by VECTSP_1:41
.= (M1 * (L + 1),i) + ((- (1_ K)) * ((((M * m,i) " ) * (M1 * (L + 1),i)) * (M * m,i))) by GROUP_1:def 4
.= (M1 * (L + 1),i) + ((- (1_ K)) * ((((M * m,i) " ) * (M * m,i)) * (M1 * (L + 1),i))) by GROUP_1:def 4
.= (M1 * (L + 1),i) + ((- (1_ K)) * ((1_ K) * (M1 * (L + 1),i))) by A15, A16, VECTSP_1:def 22
.= (M1 * (L + 1),i) + ((- (1_ K)) * (M1 * (L + 1),i)) by VECTSP_1:def 13
.= (M1 * (L + 1),i) + (- ((1_ K) * (M1 * (L + 1),i))) by VECTSP_1:41
.= (M1 * (L + 1),i) + (- (M1 * (L + 1),i)) by VECTSP_1:def 13
.= 0. K by RLVECT_1:16 ;
m <> 0 by A26;
then A32: width R = n by Th1;

per cases ( j = L + 1 or j <= L ) by A25, NAT_1:9;

suppose j = L + 1 ; :: thesis: R * j,i = 0. K

hence R * j,i = 0. K by A14, A32, A31, MATRIX_1:def 8; :: thesis: verum

end;

suppose A33: j <= L ; :: thesis: R * j,i = 0. K

then A34: j < L + 1 by NAT_1:13;
thus 0. K = M1 * j,i by A24, A26, A33
.= (Line M1,j) . i by A14, A27, MATRIX_1:def 8
.= (Line R,j) . i by A26, A34, MATRIX11:28
.= R * j,i by A14, A32, MATRIX_1:def 8 ; :: thesis: verum

end;

end;

end;

A35: S₂[ 0 ]

proof

assume 0 < m ; :: thesis: ex M1 being Matrix of m,n,K st
( Line M1,m = Line M,m & lines M1 is linearly-independent & M1 is without_repeated_line & the_rank_of M1 = the_rank_of M & ( for j being Nat st j <= 0 & j in Seg m holds
M1 * j,i = 0. K ) )
take M ; :: thesis: ( Line M,m = Line M,m & lines M is linearly-independent & M is without_repeated_line & the_rank_of M = the_rank_of M & ( for j being Nat st j <= 0 & j in Seg m holds
M * j,i = 0. K ) )
thus ( Line M,m = Line M,m & lines M is linearly-independent & M is without_repeated_line & the_rank_of M = the_rank_of M & ( for j being Nat st j <= 0 & j in Seg m holds
M * j,i = 0. K ) ) by A9, A10; :: thesis: verum

end;

for l being Nat holds S₂[l] from NAT_1:sch 2(A35, A17);
then consider M1 being Matrix of m,n,K such that
A36: Line M1,m = Line M,m and
A37: lines M1 is linearly-independent and
A38: M1 is without_repeated_line and
A39: the_rank_of M1 = the_rank_of M and
A40: for j being Nat st j <= k & j in Seg m holds
M1 * j,i = 0. K by A4;
set S = Segm M1,(Seg k),(Seg n);
A41: card (Seg k) = k by FINSEQ_1:78;
then A42: len (Segm M1,(Seg k),(Seg n)) = k by MATRIX_1:def 3;
A43: card (Seg n) = n by FINSEQ_1:78;

A44: now

A45: (Sgm (Seg n)) . i = (idseq n) . i by FINSEQ_3:54
.= i by A14, FINSEQ_2:57 ;
let j be Nat; :: thesis: ( j in Seg k implies (Segm M1,(Seg k),(Seg n)) * j,i = 0. K )
assume A46: j in Seg k ; :: thesis: (Segm M1,(Seg k),(Seg n)) * j,i = 0. K
A47: j <= k by A46, FINSEQ_1:3;
A48: (Sgm (Seg k)) . j = (idseq k) . j by FINSEQ_3:54
.= j by A46, FINSEQ_2:57 ;
width (Segm M1,(Seg k),(Seg n)) = n by A43, A46, Th1;
then [j,i] in [:(Seg k),(Seg (width (Segm M1,(Seg k),(Seg n)))):] by A14, A46, ZFMISC_1:106;
then [j,i] in Indices (Segm M1,(Seg k),(Seg n)) by A42, FINSEQ_1:def 3;
hence (Segm M1,(Seg k),(Seg n)) * j,i = M1 * ((Sgm (Seg k)) . j),((Sgm (Seg n)) . i) by Def1
.= 0. K by A40, A6, A46, A48, A45, A47 ;
:: thesis: verum

end;

set SwS = Seg (width (Segm M1,(Seg k),(Seg n)));
set SSS = Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i});
A49: width M1 = n by A3, Th1;
Segm M1,(Seg k),(Seg n) is without_repeated_line by A38, A6, Th120;
then A50: Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i}) is without_repeated_line by A41, A42, A44, Th113;
lines (Segm M1,(Seg k),(Seg n)) is linearly-independent by A37, A6, Th119;
then lines (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})) is linearly-independent by A38, A6, A41, A42, A44, Th114, Th120;
then the_rank_of (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})) = k by A2, A41, A50;
then consider P, Q being finite without_zero Subset of NAT such that
A51: [:P,Q:] c= Indices (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})) and
A52: card P = card Q and
A53: card P = k and
A54: Det (EqSegm (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})),P,Q) <> 0. K by Def4;
( P = {} iff Q = {} ) by A52;
then consider P1, Q1 being finite without_zero Subset of NAT such that
A55: P1 c= Seg k and
A56: Q1 c= (Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i} and
P1 = (Sgm (Seg k)) .: P and
Q1 = (Sgm ((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})) .: Q and
A57: card P1 = card P and
A58: card Q1 = card Q and
A59: Segm (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})),P,Q = Segm (Segm M1,(Seg k),(Seg n)),P1,Q1 by A51, Th57;
(Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i} c= Seg (width (Segm M1,(Seg k),(Seg n))) by XBOOLE_1:36;
then A60: Q1 c= Seg (width (Segm M1,(Seg k),(Seg n))) by A56, XBOOLE_1:1;
then [:P1,Q1:] c= [:(Seg k),(Seg (width (Segm M1,(Seg k),(Seg n)))):] by A55, ZFMISC_1:119;
then A61: [:P1,Q1:] c= Indices (Segm M1,(Seg k),(Seg n)) by A42, FINSEQ_1:def 3;

A62: now

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: Q1 c= Seg n

then width (Segm M1,(Seg k),(Seg n)) = 0 by A42, MATRIX_1:def 4;
then Seg (width (Segm M1,(Seg k),(Seg n))) c= Seg n by FINSEQ_1:7;
hence Q1 c= Seg n by A60, XBOOLE_1:1; :: thesis: verum

end;

suppose k > 0 ; :: thesis: Q1 c= Seg n

hence Q1 c= Seg n by A43, A60, Th1; :: thesis: verum

end;

end;

end;

( P1 = {} iff Q1 = {} ) by A52, A57, A58;
then consider P2, Q2 being finite without_zero Subset of NAT such that
A63: P2 c= Seg k and
A64: Q2 c= Seg n and
A65: P2 = (Sgm (Seg k)) .: P1 and
A66: Q2 = (Sgm (Seg n)) .: Q1 and
A67: card P2 = card P1 and
A68: card Q2 = card Q1 and
A69: Segm (Segm M1,(Seg k),(Seg n)),P1,Q1 = Segm M1,P2,Q2 by A61, Th57;
A70: Q2 = (idseq n) .: Q1 by A66, FINSEQ_3:54
.= Q1 by A62, FRECHET:13 ;
reconsider i = i, m = m as non zero Element of NAT by A3, A11, ORDINAL1:def 13;
set Q2i = Q2 \/ {i};
set SQ2i = Sgm (Q2 \/ {i});
A71: {i} c= Seg n by A14, ZFMISC_1:37;
then A72: Q2 \/ {i} c= Seg n by A64, XBOOLE_1:8;
then A73: rng (Sgm (Q2 \/ {i})) = Q2 \/ {i} by FINSEQ_1:def 13;
A74: P2 = (idseq k) .: P1 by A65, FINSEQ_3:54
.= P1 by A55, FRECHET:13 ;
A75: EqSegm (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})),P,Q = Segm (Segm M1,(Seg k),(Seg n)),P1,Q1 by A52, A59, Def3
.= EqSegm M1,P1,Q1 by A52, A57, A58, A69, A74, A70, Def3 ;
A76: len (EqSegm M1,P2,Q2) = k by A53, A57, A67, MATRIX_1:def 3;
A77: len M1 = m by Th1;
then A78: the_rank_of M1 <= m by Th74;
set P2m = P2 \/ {m};
set ES = EqSegm M1,(P2 \/ {m}),(Q2 \/ {i});
A79: P2 c= Seg m by A6, A63, XBOOLE_1:1;
i in {i} by TARSKI:def 1;
then A80: i in Q2 \/ {i} by XBOOLE_0:def 3;
i in {i} by TARSKI:def 1;
then A81: not i in Q2 by A56, A70, XBOOLE_0:def 5;
then A82: card (Q2 \/ {i}) = m by A3, A52, A53, A58, A68, CARD_2:54;
then dom (Sgm (Q2 \/ {i})) = Seg m by A64, A71, FINSEQ_3:45, XBOOLE_1:8;
then consider Si being set such that
A83: Si in Seg m and
A84: (Sgm (Q2 \/ {i})) . Si = i by A80, A73, FUNCT_1:def 5;
reconsider Si = Si as Element of NAT by A83;
k < m by A3, NAT_1:13;
then A85: not m in P2 by A55, A74, FINSEQ_1:3;
then A86: card (P2 \/ {m}) = m by A3, A53, A57, A67, CARD_2:54;
then A87: len (Delete (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),m,Si) = m -' 1 by MATRIX_1:def 3;
A88: {m} c= Seg m by A7, ZFMISC_1:37;
then P2 \/ {m} c= Seg m by A79, XBOOLE_1:8;
then [:(P2 \/ {m}),(Q2 \/ {i}):] c= [:(Seg m),(Seg n):] by A72, ZFMISC_1:119;
then A89: [:(P2 \/ {m}),(Q2 \/ {i}):] c= Indices M1 by A77, A49, FINSEQ_1:def 3;
card (Seg m) = m by FINSEQ_1:78;
then A90: P2 \/ {m} = Seg m by A88, A79, A86, CARD_FIN:1, XBOOLE_1:8;

A91: now

A92: dom (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) = Seg (len (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i}))) by FINSEQ_1:def 3;
A93: dom M1 = Seg (len M1) by FINSEQ_1:def 3;
A94: m = len (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) by A86, MATRIX_1:def 3;
let j be Nat; :: thesis: ( j in Seg m implies (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si = M1 * j,i )
assume A95: j in Seg m ; :: thesis: (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si = M1 * j,i
Col M1,i = Col (Segm M1,(P2 \/ {m}),(Q2 \/ {i})),Si by A77, A82, A83, A84, A90, Th50
.= Col (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si by A3, A53, A57, A67, A85, A82, Def3, CARD_2:54 ;
hence (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si = (Col M1,i) . j by A95, A94, A92, MATRIX_1:def 9
.= M1 * j,i by A77, A95, A93, MATRIX_1:def 9 ;
:: thesis: verum

end;

then A96: (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * m,Si = M1 * m,i by A3, FINSEQ_1:6
.= (Line M,m) . i by A14, A36, A49, MATRIX_1:def 8 ;
set LC = LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si;
len (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) = m by A86, LAPLACE:def 8;
then A97: dom (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) = Seg m by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in Seg m & j <> m implies 0. K = (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) . j )
assume that
A98: j in Seg m and
A99: j <> m ; :: thesis: 0. K = (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) . j
reconsider J = j as Element of NAT by ORDINAL1:def 13;
j <= m by A98, FINSEQ_1:3;
then j <= k by A3, A99, NAT_1:9;
then 0. K = M1 * j,i by A40, A98
.= (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si by A91, A98 ;
hence 0. K = ((EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si) * (Cofactor (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),J,Si) by VECTSP_1:39
.= (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) . j by A97, A98, LAPLACE:def 8 ;
:: thesis: verum

end;

then A100: (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) . m = Sum (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) by A7, A97, MATRIX_3:14
.= Det (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) by A86, A83, LAPLACE:27 ;
reconsider mSi = m + Si as Element of NAT ;
- (1_ K) <> 0. K by VECTSP_1:86;
then A101: (power K) . (- (1_ K)),mSi <> 0. K by Lm6;
(Sgm (P2 \/ {m})) . m = (idseq m) . m by A90, FINSEQ_3:54
.= m by A7, FINSEQ_2:57 ;
then Delete (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),m,Si = EqSegm M1,((P2 \/ {m}) \ {m}),((Q2 \/ {i}) \ {i}) by A7, A86, A82, A83, A84, Th64
.= EqSegm M1,P2,((Q2 \/ {i}) \ {i}) by A85, ZFMISC_1:141
.= EqSegm M1,P2,Q2 by A81, ZFMISC_1:141 ;
then ((power K) . (- (1_ K)),mSi) * (Minor (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),m,Si) <> 0. K by A53, A54, A74, A70, A75, A86, A87, A76, A101, VECTSP_1:44;
then ((EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * m,Si) * (Cofactor (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),m,Si) <> 0. K by A15, A96, VECTSP_1:44;
then Det (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) <> 0. K by A7, A97, A100, LAPLACE:def 8;
then the_rank_of M1 >= m by A89, A86, A82, Def4;
hence the_rank_of M = m by A39, A78, XXREAL_0:1; :: thesis: verum

end;

thus ( the_rank_of M = m implies ( lines M is linearly-independent & M is without_repeated_line ) ) by Th105, Th110; :: thesis: verum

end;

A102: S₁[ 0 ]

proof

let m, n be Nat; :: thesis: ( m = 0 implies for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m ) )
assume A103: m = 0 ; :: thesis: for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
let M be Matrix of m,n,K; :: thesis: ( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
A104: len M = 0 by A103, MATRIX_1:def 3;
then M = {} ;
hence ( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m ) by A103, A104, Th74; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A102, A1);
hence for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m ) ; :: thesis: verum