let m, n be Nat; :: thesis:
let K be Field; :: thesis:
let M be Matrix of m,n,K; :: thesis:
let i be Nat; :: thesis:
assume that
A1: M is without_repeated_line and
A2: lines M is linearly-independent and
A3: for j being Nat st j in Seg m holds
M * (j,i) = 0. K ; :: thesis:
set SMi = (Seg (width M)) \ {i};
set Sl = Seg (len M);
set S = Segm (M,(Seg (len M)),((Seg (width M)) \ {i}));
A4: (Seg (width M)) \ {i} c= Seg (width M) by XBOOLE_1:36;
A5: card (Seg (len M)) = len M by FINSEQ_1:57;
A6: len M = m by MATRIX_0:def 2;

per cases ;

suppose m = 0 ; :: thesis:

then len (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) = 0 by A6, MATRIX_0:def 2;
then Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = {} ;
hence lines (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) is linearly-independent ; :: thesis:

end;

suppose m <> 0 ; :: thesis:

then A7: width M = n by Th1;

A8: now :: thesis:

end;

A23: now :: thesis:

set NULL = 0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})));
let M1 be Matrix of card (Seg (len M)), card ((Seg (width M)) \ {i}),K; :: thesis:
assume that
A24: for i being Nat st i in Seg (card (Seg (len M))) holds
ex a being Element of K st Line (M1,i) = a * (Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),i)) and
A25: for j being Nat st j in Seg (card ((Seg (width M)) \ {i})) holds
Sum (Col (M1,j)) = 0. K ; :: thesis:
defpred S₁[ set , set ] means for i being Nat st $1 = i holds
ex a being Element of K st
( a = $2 & Line (M1,i) = a * (Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),i)) );
A26: for k being Nat st k in Seg m holds
ex x being Element of K st S₁[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg m ; :: thesis:
then consider a being Element of K such that
A27: Line (M1,k) = a * (Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),k)) by A5, A6, A24;
take a ; :: thesis:
thus S₁[k,a] by A27; :: thesis:

end;

consider p being FinSequence of K such that
A28: dom p = Seg m and
A29: for k being Nat st k in Seg m holds
S₁[k,p . k] from FINSEQ_1:sch 5(A26);
deffunc H₁( Nat) -> Element of (width M) -tuples_on the carrier of K = (p /. $1) * (Line (M,$1));
consider f being FinSequence of (width M) -tuples_on the carrier of K such that
A30: len f = m and
A31: for j being Nat st j in dom f holds
f . j = H₁(j) from FINSEQ_2:sch 1();
reconsider f9 = f as FinSequence of the carrier of (n -VectSp_over K) by A7, Th102;
FinS2MX f9 is Matrix of m,n,K by A30;
then reconsider Mf = f as Matrix of m,n,K ;
A32: dom f = Seg m by A30, FINSEQ_1:def 3;
len Mf = m by MATRIX_0:def 2;
then A33: dom Mf = Seg m by FINSEQ_1:def 3;

A34: now :: thesis:

A35: len M1 = m by A5, A6, MATRIX_0:def 2;
A36: len Mf = m by MATRIX_0:def 2;
A37: dom Mf = Seg (len Mf) by FINSEQ_1:def 3;
A38: dom M1 = Seg (len M1) by FINSEQ_1:def 3;
let j be Nat; :: thesis:
assume A39: j in Seg n ; :: thesis:
set C = Col (Mf,j);
A40: len (Col (Mf,j)) = len Mf by MATRIX_0:def 8
.= m by MATRIX_0:def 2 ;

per cases ;

suppose A41: j = i ; :: thesis:

set m0 = m |-> (0. K);

A42: now :: thesis:

let n9 be Nat; :: thesis:
assume that
A43: 1 <= n9 and
A44: n9 <= m ; :: thesis:
A45: width M = n by A43, A44, Th1;
A46: width Mf = n by A43, A44, Th1;
A47: n9 in Seg m by A43, A44;
then A48: Mf . n9 = Mf /. n9 by A33, PARTFUN1:def 6;
0. K = M * (n9,i) by A3, A47
.= (Line (M,n9)) . i by A39, A41, A45, MATRIX_0:def 7 ;
then (p /. n9) * (0. K) = ((p /. n9) * (Line (M,n9))) . i by A39, A41, A45, FVSUM_1:51
.= (Mf /. n9) . i by A31, A32, A47, A48
.= (Line (Mf,n9)) . i by A47, A48, MATRIX_0:52
.= Mf * (n9,i) by A39, A41, A46, MATRIX_0:def 7
.= (Col (Mf,i)) . n9 by A36, A37, A47, MATRIX_0:def 8 ;
hence (Col (Mf,j)) . n9 = 0. K by A41
.= (m |-> (0. K)) . n9 by A47, FINSEQ_2:57 ;
:: thesis:

end;

len (m |-> (0. K)) = m by CARD_1:def 7;
then Col (Mf,j) = m |-> (0. K) by A40, A42;
hence Sum (Col (Mf,j)) = 0. K by A40, MATRIX_3:11; :: thesis:

end;

suppose A49: j <> i ; :: thesis:

A50: rng (Sgm ((Seg (width M)) \ {i})) = (Seg (width M)) \ {i} by A4, FINSEQ_1:def 13;
j in (Seg (width M)) \ {i} by A7, A39, A49, ZFMISC_1:56;
then consider x being object such that
A51: x in dom (Sgm ((Seg (width M)) \ {i})) and
A52: (Sgm ((Seg (width M)) \ {i})) . x = j by A50, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A51;
set C1 = Col (M1,x);
A53: dom (Sgm ((Seg (width M)) \ {i})) = Seg (card ((Seg (width M)) \ {i})) by FINSEQ_3:40, XBOOLE_1:36;

A54: now :: thesis:

let n9 be Nat; :: thesis:
assume that
A55: 1 <= n9 and
A56: n9 <= m ; :: thesis:
A57: width Mf = n by A55, A56, Th1;
A58: width (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) = card ((Seg (width M)) \ {i}) by A6, A55, A56, Th1;
A59: Sgm (Seg (len M)) = idseq m by A6, FINSEQ_3:48;
A60: width M1 = card ((Seg (width M)) \ {i}) by A6, A55, A56, Th1;
A61: (Line (M,n9)) . j = M * (n9,j) by A7, A39, MATRIX_0:def 7;
A62: n9 in Seg m by A55, A56;
then consider a being Element of K such that
A63: a = p . n9 and
A64: Line (M1,n9) = a * (Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),n9)) by A29;
A65: Mf . n9 = Mf /. n9 by A33, A62, PARTFUN1:def 6;
(idseq m) . n9 = n9 by A62, FINSEQ_2:49;
then (Line (M,n9)) * (Sgm ((Seg (width M)) \ {i})) = Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),n9) by A5, A6, A62, A59, Th47, XBOOLE_1:36;
then A66: (Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),n9)) . x = (Line (M,n9)) . j by A51, A52, FUNCT_1:13;
thus (Col (Mf,j)) . n9 = Mf * (n9,j) by A36, A37, A62, MATRIX_0:def 8
.= (Line (Mf,n9)) . j by A39, A57, MATRIX_0:def 7
.= (Mf /. n9) . j by A62, A65, MATRIX_0:52
.= ((p /. n9) * (Line (M,n9))) . j by A31, A32, A62, A65
.= (a * (Line (M,n9))) . j by A28, A62, A63, PARTFUN1:def 6
.= a * (M * (n9,j)) by A7, A39, A61, FVSUM_1:51
.= (a * (Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),n9))) . x by A51, A53, A58, A66, A61, FVSUM_1:51
.= M1 * (n9,x) by A51, A53, A60, A64, MATRIX_0:def 7
.= (Col (M1,x)) . n9 by A35, A38, A62, MATRIX_0:def 8 ; :: thesis:

end;

A67: len (Col (Mf,j)) = len Mf by MATRIX_0:def 8;
len (Col (M1,x)) = len M1 by MATRIX_0:def 8;
then Col (Mf,j) = Col (M1,x) by A36, A35, A67, A54;
hence Sum (Col (Mf,j)) = 0. K by A25, A51, A53; :: thesis:

end;

now :: thesis:

let j be Nat; :: thesis:
assume A68: j in Seg m ; :: thesis:
take pj = p /. j; :: thesis:
thus Line (Mf,j) = Mf . j by A68, MATRIX_0:52
.= pj * (Line (M,j)) by A31, A32, A68 ; :: thesis:

end;

then A69: Mf = 0. (K,m,n) by A1, A2, A34, Th109;

A70: now :: thesis:

let j be Nat; :: thesis:
assume that
A71: 1 <= j and
A72: j <= m ; :: thesis:
A73: j in Seg m by A71, A72;
then consider a being Element of K such that
A74: a = p . j and
A75: Line (M1,j) = a * (Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),j)) by A29;
A76: Line ((0. (K,m,n)),j) = (0. (K,m,n)) . j by A73, MATRIX_0:52
.= n |-> (0. K) by A73, FUNCOP_1:7 ;
p . j = p /. j by A28, A73, PARTFUN1:def 6;
then A77: a * (Line (M,j)) = Mf . j by A31, A32, A73, A74
.= Line (Mf,j) by A73, MATRIX_0:52 ;
A78: rng (Sgm ((Seg (width M)) \ {i})) = (Seg (width M)) \ {i} by A4, FINSEQ_1:def 13;
Sgm (Seg (len M)) = idseq m by A6, FINSEQ_3:48;
then (Sgm (Seg (len M))) . j = j by A73, FINSEQ_2:49;
then A79: Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),j) = (Line (M,j)) * (Sgm ((Seg (width M)) \ {i})) by A5, A6, A73, Th47, XBOOLE_1:36;
(Seg n) /\ ((Seg (width M)) \ {i}) = (Seg (width M)) \ {i} by A7, XBOOLE_1:28, XBOOLE_1:36;
then A80: (Sgm ((Seg (width M)) \ {i})) " (Seg n) = (Sgm ((Seg (width M)) \ {i})) " (rng (Sgm ((Seg (width M)) \ {i}))) by A78, RELAT_1:133
.= dom (Sgm ((Seg (width M)) \ {i})) by RELAT_1:134
.= Seg (card ((Seg (width M)) \ {i})) by FINSEQ_3:40, XBOOLE_1:36 ;
dom (Line (M,j)) = Seg (len (Line (M,j))) by FINSEQ_1:def 3
.= Seg (width M) by CARD_1:def 7 ;
then Line (M1,j) = (Line ((0. (K,m,n)),j)) * (Sgm ((Seg (width M)) \ {i})) by A69, A75, A77, A78, A79, Th87, XBOOLE_1:36
.= (card ((Seg (width M)) \ {i})) |-> (0. K) by A80, A76, FUNCOP_1:19
.= (0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})))) . j by A5, A6, A73, FUNCOP_1:7 ;
hence M1 . j = (0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})))) . j by A5, A6, A73, MATRIX_0:52; :: thesis:

end;

A81: len (0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})))) = m by A5, A6, MATRIX_0:def 2;
len M1 = m by A5, A6, MATRIX_0:def 2;
hence M1 = 0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i}))) by A81, A70; :: thesis:

end;

Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) is without_repeated_line by A1, A3, Th113;
hence lines (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) is linearly-independent by A8, A23, Th109; :: thesis:

end;