let n, m be Nat; :: thesis:
let K be Field; :: thesis:
let M be Matrix of m,n,K; :: thesis:
assume A1: M is without_repeated_line ; :: thesis:
thus ( ( for i being Nat st i in Seg m holds
Line M,i <> n |-> (0. K) ) & ( 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) ) & ( for j being Nat st j in Seg n holds
Sum (Col M1,j) = 0. K ) holds
M1 = 0. K,m,n ) implies lines M is linearly-independent ) :: thesis:

assume that
A2: for i being Nat st i in Seg m holds
Line M,i <> n |-> (0. K) and
A3: 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) ) & ( for j being Nat st j in Seg n holds
Sum (Col M1,j) = 0. K ) holds
M1 = 0. K,m,n ; :: thesis:
set V = n -VectSp_over K;
A4: n in NAT by ORDINAL1:def 13;
let L be Linear_Combination of lines M; :: according to VECTSP_7:def 1 :: thesis:
assume A5: Sum L = 0. (n -VectSp_over K) ; :: thesis:
set MX = MX2FinS M;
set LM = L (#) (MX2FinS M);
set FLM = FinS2MX (L (#) (MX2FinS M));
A6: ( len M = m & len M = len (L (#) (MX2FinS M)) ) by MATRIX_1:def 3, VECTSP_6:def 8;
then reconsider flm = FinS2MX (L (#) (MX2FinS M)) as Matrix of m,n,K ;
A7: for i being Nat st i in Seg m holds
ex a being Element of K st Line flm,i = a * (Line M,i)

let i be Nat; :: thesis:
assume A8: i in Seg m ; :: thesis:
Line M,i in lines M by A8, Th103;
then reconsider LM = Line M,i as Element of (n -VectSp_over K) ;
reconsider LLM = L . LM as Element of K ;
Line M,i = M . i by A8, MATRIX_2:10;
then Line flm,i = LLM * (Line M,i) by A6, A8, Th106;
hence ex a being Element of K st Line flm,i = a * (Line M,i) ; :: thesis:

end;

now

let j be Nat; :: thesis:
assume A9: j in Seg n ; :: thesis:
Carrier L c= lines M by VECTSP_6:def 7;
then ( (Sum L) . j = Sum (Col flm,j) & (n |-> (0. K)) . j = 0. K ) by A1, A9, Th107, FINSEQ_2:71;
hence Sum (Col flm,j) = 0. K by A5, Th102; :: thesis:

end;

then A10: flm = 0. K,m,n by A3, A7;
assume Carrier L <> {} ; :: thesis:
then consider x being set such that
A11: x in Carrier L by XBOOLE_0:def 1;
Carrier L c= lines M by VECTSP_6:def 7;
then consider i being Nat such that
A12: ( i in Seg m & x = Line M,i ) by A11, Th103;
consider v being Vector of (n -VectSp_over K) such that
A13: ( x = v & L . v <> 0. K ) by A11, VECTSP_6:19;
reconsider LM = Line M,i as Element of n -tuples_on the carrier of K by A12, A13, Th102;
( LM <> n |-> (0. K) & len LM = n & len (n |-> (0. K)) = n ) by A2, A12, FINSEQ_1:def 18;
then consider j being Nat such that
A14: ( 1 <= j & j <= n & LM . j <> (n |-> (0. K)) . j ) by FINSEQ_1:18;
A15: j in NAT by ORDINAL1:def 13;
then ( j in Seg n & dom LM = Seg n ) by A14, FINSEQ_2:144;
then ( LM . j in rng LM & rng LM c= the carrier of K ) by FUNCT_1:def 5, RELAT_1:def 19;
then reconsider LMj = LM . j as Element of K ;
A16: ( flm . i = n |-> (0. K) & flm . i = Line flm,i ) by A10, A12, FUNCOP_1:13, MATRIX_2:10;
( j in Seg n & Line M,i = M . i ) by A12, A14, A15, MATRIX_2:10;
then ( LM . j <> 0. K & ((L . v) * LM) . j = (L . v) * LMj & Line flm,i = (L . v) * LM & (Line flm,i) . j = 0. K ) by A4, A6, A12, A13, A14, A16, Th106, FINSEQ_2:71, FVSUM_1:63;
hence contradiction by A13, VECTSP_1:44; :: thesis:

end;

assume A17: lines M is linearly-independent ; :: thesis:
set V = n -VectSp_over K;

hereby :: thesis:

let i be Nat; :: thesis:
assume A18: i in Seg m ; :: thesis:
Line M,i in lines M by A18, Th103;
then Line M,i <> 0. (n -VectSp_over K) by A17, VECTSP_7:3;
hence Line M,i <> n |-> (0. K) by Th102; :: thesis:

end;

let M1 be Matrix of m,n,K; :: thesis:
assume that
A19: for i being Nat st i in Seg m holds
ex a being Element of K st Line M1,i = a * (Line M,i) and
A20: for j being Nat st j in Seg n holds
Sum (Col M1,j) = 0. K ; :: thesis:
consider L being Linear_Combination of lines M such that
A21: L (#) (MX2FinS M) = M1 by A1, A19, Th108;
reconsider SumL = Sum L as Element of n -tuples_on the carrier of K by Th102;
A22: Carrier L c= lines M by VECTSP_6:def 7;
set n0 = n |-> (0. K);
A23: ( len SumL = n & len (n |-> (0. K)) = n ) by FINSEQ_1:def 18;

let j be Nat; :: thesis:
assume A24: ( 1 <= j & j <= n ) ; :: thesis:
j in NAT by ORDINAL1:def 13;
then A25: j in Seg n by A24;
hence (Sum L) . j = Sum (Col (FinS2MX (L (#) (MX2FinS M))),j) by A1, A22, Th107
.= 0. K by A20, A21, A25
.= (n |-> (0. K)) . j by A25, FINSEQ_2:71 ;
:: thesis:

end;

then SumL = n |-> (0. K) by A23, FINSEQ_1:18
.= 0. (n -VectSp_over K) by Th102 ;
then A26: Carrier L = {} by A17, VECTSP_7:def 1;
assume M1 <> 0. K,m,n ; :: thesis:
then consider I, J being Nat such that
A27: ( [I,J] in Indices M1 & M1 * I,J <> (0. K,m,n) * I,J ) by MATRIX_1:28;
reconsider ii = I, jj = J as Element of NAT by ORDINAL1:def 13;
[I,J] in Indices (0. K,m,n) by A27, MATRIX_1:27;
then A28: M1 * I,J <> 0. K by A27, MATRIX_3:3;
Indices M1 = Indices M by MATRIX_1:27;
then ( Indices M1 = [:(Seg (len M)),(Seg (width M)):] & Indices M1 = [:(Seg (len M1)),(Seg (width M1)):] ) by FINSEQ_1:def 3;
then A29: ( ii in Seg (len M) & jj in Seg (width M) & jj in Seg (width M1) & len M = m ) by A27, MATRIX_1:def 3, ZFMISC_1:106;
then ( M . ii = Line M,ii & Line M,ii in lines M ) by Th103, MATRIX_2:10;
then reconsider Mii = M . ii as Element of (n -VectSp_over K) ;
A30: (Line M,ii) . jj = M * ii,jj by A29, MATRIX_1:def 8;
M1 * I,J = (Line (FinS2MX (L (#) (MX2FinS M))),ii) . jj by A21, A29, MATRIX_1:def 8
.= ((L . Mii) * (Line M,ii)) . jj by A29, Th106
.= (L . Mii) * (M * ii,jj) by A29, A30, FVSUM_1:63 ;
then L . Mii <> 0. K by A28, VECTSP_1:44;
hence contradiction by A26, VECTSP_6:19; :: thesis: