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 S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[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 CARD_1:def 7;
k < m by A3, NAT_1:13;
then A6: Seg k c= Seg m by FINSEQ_1:5;
A7: m in Seg m by A3, FINSEQ_1:4;
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 CARD_1:def 7;
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;
defpred S2[ 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 ) ) );
A14: i in Seg n by A11, A12;
then A15: LM . i <> 0. K by A13, FINSEQ_2:57;
len (Line (M,m)) = width M by MATRIX_0:def 7;
then A16: LM . i = M * (m,i) by A8, A14, MATRIX_0:def 7;
A17: for l being Nat st S2[l] holds
S2[l + 1]
proof
set Mmi = M * (m,i);
let L be Nat; :: thesis: ( S2[L] implies S2[L + 1] )
assume A18: S2[L] ; :: thesis: S2[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_0:def 2;
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_0:def 7;
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 CARD_1:def 7;
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_0:def 7;
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:51;
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:18
.= (M1 * ((L + 1),i)) + ((- ((1_ K) * (((M * (m,i)) ") * (M1 * ((L + 1),i))))) * (M * (m,i)))
.= (M1 * ((L + 1),i)) + (((- (1_ K)) * (((M * (m,i)) ") * (M1 * ((L + 1),i)))) * (M * (m,i))) by VECTSP_1:9
.= (M1 * ((L + 1),i)) + ((- (1_ K)) * ((((M * (m,i)) ") * (M1 * ((L + 1),i))) * (M * (m,i)))) by GROUP_1:def 3
.= (M1 * ((L + 1),i)) + ((- (1_ K)) * ((((M * (m,i)) ") * (M * (m,i))) * (M1 * ((L + 1),i)))) by GROUP_1:def 3
.= (M1 * ((L + 1),i)) + ((- (1_ K)) * ((1_ K) * (M1 * ((L + 1),i)))) by A15, A16, VECTSP_1:def 10
.= (M1 * ((L + 1),i)) + ((- (1_ K)) * (M1 * ((L + 1),i)))
.= (M1 * ((L + 1),i)) + (- ((1_ K) * (M1 * ((L + 1),i)))) by VECTSP_1:9
.= (M1 * ((L + 1),i)) + (- (M1 * ((L + 1),i)))
.= 0. K by RLVECT_1:5 ;
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_0:def 7; :: 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_0:def 7
.= (Line (R,j)) . i by A26, A34, MATRIX11:28
.= R * (j,i) by A14, A32, MATRIX_0:def 7 ; :: thesis: verum
end;
end;
end;
A35: S2[ 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 S2[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:57;
then A42: len (Segm (M1,(Seg k),(Seg n))) = k by MATRIX_0:def 2;
A43: card (Seg n) = n by FINSEQ_1:57;
A44: now :: thesis: for j being Nat st j in Seg k holds
(Segm (M1,(Seg k),(Seg n))) * (j,i) = 0. K
A45: (Sgm (Seg n)) . i = (idseq n) . i by FINSEQ_3:48
.= i by A14, FINSEQ_2:49 ;
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:1;
A48: (Sgm (Seg k)) . j = (idseq k) . j by FINSEQ_3:48
.= j by A46, FINSEQ_2:49 ;
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:87;
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;
then [:P1,Q1:] c= [:(Seg k),(Seg (width (Segm (M1,(Seg k),(Seg n))))):] by A55, ZFMISC_1:96;
then A61: [:P1,Q1:] c= Indices (Segm (M1,(Seg k),(Seg n))) by A42, FINSEQ_1:def 3;
A62: now :: thesis: Q1 c= Seg n
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_0:def 3;
then Seg (width (Segm (M1,(Seg k),(Seg n)))) c= Seg n ;
hence Q1 c= Seg n by A60; :: 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:48
.= Q1 by A62, FRECHET:13 ;
reconsider i = i, m = m as non zero Element of NAT by A3, A11, ORDINAL1:def 12;
set Q2i = Q2 \/ {i};
set SQ2i = Sgm (Q2 \/ {i});
{i} c= Seg n by A14, ZFMISC_1:31;
then A72: Q2 \/ {i} c= Seg n by A64, XBOOLE_1:8;
A73: rng (Sgm (Q2 \/ {i})) = Q2 \/ {i} by FINSEQ_1:def 14;
A74: P2 = (idseq k) .: P1 by A65, FINSEQ_3:48
.= 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_0:def 2;
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;
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:41;
then dom (Sgm (Q2 \/ {i})) = Seg m by FINSEQ_3:40;
then consider Si being object such that
A83: Si in Seg m and
A84: (Sgm (Q2 \/ {i})) . Si = i by A80, A73, FUNCT_1:def 3;
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:1;
then A86: card (P2 \/ {m}) = m by A3, A53, A57, A67, CARD_2:41;
then A87: len (Delete ((EqSegm (M1,(P2 \/ {m}),(Q2 \/ {i}))),m,Si)) = m -' 1 by MATRIX_0:def 2;
A88: {m} c= Seg m by A7, ZFMISC_1:31;
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:96;
then A89: [:(P2 \/ {m}),(Q2 \/ {i}):] c= Indices M1 by A77, A49, FINSEQ_1:def 3;
card (Seg m) = m by FINSEQ_1:57;
then A90: P2 \/ {m} = Seg m by A88, A79, A86, CARD_2:102, XBOOLE_1:8;
A91: now :: thesis: for j being Nat st j in Seg m holds
(EqSegm (M1,(P2 \/ {m}),(Q2 \/ {i}))) * (j,Si) = M1 * (j,i)
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_0:def 2;
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:41 ;
hence (EqSegm (M1,(P2 \/ {m}),(Q2 \/ {i}))) * (j,Si) = (Col (M1,i)) . j by A95, A94, A92, MATRIX_0:def 8
.= M1 * (j,i) by A77, A95, A93, MATRIX_0:def 8 ;
:: thesis: verum
end;
then A96: (EqSegm (M1,(P2 \/ {m}),(Q2 \/ {i}))) * (m,Si) = M1 * (m,i) by A3, FINSEQ_1:4
.= (Line (M,m)) . i by A14, A36, A49, MATRIX_0:def 7 ;
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 :: thesis: for j being Nat st j in Seg m & j <> m holds
0. K = (LaplaceExpC ((EqSegm (M1,(P2 \/ {m}),(Q2 \/ {i}))),Si)) . j
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 12;
j <= m by A98, FINSEQ_1:1;
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))
.= (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:12
.= 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:28;
then A101: (power K) . ((- (1_ K)),mSi) <> 0. K by Lm6;
(Sgm (P2 \/ {m})) . m = (idseq m) . m by A90, FINSEQ_3:48
.= m by A7, FINSEQ_2:49 ;
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:117
.= EqSegm (M1,P2,Q2) by A81, ZFMISC_1:117 ;
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:12;
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:12;
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: S1[ 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 )
len M = 0 by A103, MATRIX_0:def 2;
then M = {} ;
hence ( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m ) by A103, Th74; :: thesis: verum
end;
for k being Nat holds S1[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