let m, n be Nat; :: thesis:
let K be Field; :: thesis:
let A be Matrix of n,m,K; :: thesis:
let N be finite without_zero Subset of NAT; :: thesis:
assume that
A1: card N = n and
A2: N c= Seg m and
A3: Segm (A,(Seg n),N) = 1. (K,n) and
A4: n > 0 and
A5: m -' n > 0 ; :: thesis:
Seg m <> {} by A1, A2, A4, CARD_1:27, XBOOLE_1:3;
then A6: m <> 0 ;
consider MV being Matrix of m -' n,m,K such that
A7: Segm (MV,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) and
A8: Segm (MV,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) and
A9: for l being Nat
for M being Matrix of m,l,K st ( for i being Nat holds
( not i in Seg l or ex j being Nat st
( j in Seg (m -' n) & Col (M,i) = Line (MV,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l))) by A1, A2, A3, A4, Th49;
A10: width MV = m by A5, MATRIX_0:23;
A11: ( len MV = m -' n & len MV >= the_rank_of MV ) by MATRIX13:74, MATRIX_0:def 2;
A12: Indices MV = [:(Seg (m -' n)),(Seg m):] by A5, MATRIX_0:23;
(Seg m) \ N c= Seg m by XBOOLE_1:36;
then A13: [:(Seg (m -' n)),((Seg m) \ N):] c= Indices MV by A12, ZFMISC_1:95;
A14: width A = m by A4, MATRIX_0:23;
A15: len A = n by A4, MATRIX_0:23;
lines MV c= Solutions_of (A,((len A) |-> (0. K)))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in lines MV ; :: thesis:
then consider k being Nat such that
A16: k in Seg (m -' n) and
A17: x = Line (MV,k) by MATRIX13:103;
set C = ColVec2Mx (Line (MV,k));
A18: m = width MV by A5, MATRIX_0:23
.= len (Line (MV,k)) by CARD_1:def 7 ;

now :: thesis:

let i be Nat; :: thesis:
assume i in Seg 1 ; :: thesis:
then A19: i = 1 by FINSEQ_1:2, TARSKI:def 1;
Col ((ColVec2Mx (Line (MV,k))),1) = Line (MV,k) by A6, A18, Th26;
hence ( ex j being Nat st
( j in Seg (m -' n) & Col ((ColVec2Mx (Line (MV,k))),i) = Line (MV,j) ) or Col ((ColVec2Mx (Line (MV,k))),i) = m |-> (0. K) ) by A16, A19; :: thesis:

end;

then ColVec2Mx (Line (MV,k)) in Solutions_of (A,(0. (K,n,1))) by A9, A18;
then ColVec2Mx (Line (MV,k)) in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) by A15, Th32;
hence x in Solutions_of (A,((len A) |-> (0. K))) by A17; :: thesis:

end;

then Lin (lines MV) is Subspace of Lin (Solutions_of (A,((len A) |-> (0. K)))) by A14, VECTSP_7:13;
then A20: the carrier of (Lin (lines MV)) c= the carrier of (Lin (Solutions_of (A,((len A) |-> (0. K))))) by VECTSP_4:def 2;
(m -' n) + 0 > 0 by A5;
then m -' n >= 1 by NAT_1:19;
then A21: Det (1. (K,(m -' n))) = 1_ K by MATRIX_7:16;
A22: 0. K <> 1_ K ;
A23: card (Seg m) = m by FINSEQ_1:57;
then A24: m -' n = m - n by A1, A2, NAT_1:43, XREAL_1:233;
A25: card ((Seg m) \ N) = m - n by A1, A2, A23, CARD_2:44;
then A26: card (Seg (m -' n)) = card ((Seg m) \ N) by A24, FINSEQ_1:57;
EqSegm (MV,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) by A7, A24, A25, FINSEQ_1:57, MATRIX13:def 3;
then m -' n <= the_rank_of MV by A24, A25, A26, A13, A21, A22, MATRIX13:def 4;
then A27: the_rank_of MV = m -' n by A11, XXREAL_0:1;
A28: the carrier of (Space_of_Solutions_of A) c= the carrier of (Lin (lines MV))

proof

set SN = (Seg m) \ N;
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in the carrier of (Space_of_Solutions_of A) ; :: thesis:
then y in Solutions_of (A,((len A) |-> (0. K))) by A6, A14, Def5;
then consider f being FinSequence of K such that
A29: f = y and
A30: ColVec2Mx f in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) ;
A31: len f = m by A14, A30, Th59;
deffunc H₁( Nat) -> Element of (width MV) -tuples_on the carrier of K = (f /. ((Sgm ((Seg m) \ N)) . $1)) * (Line (MV,$1));
A32: dom f = Seg (len f) by FINSEQ_1:def 3;
consider M being FinSequence of (width MV) -tuples_on the carrier of K such that
A33: len M = m -' n and
A34: for j being Nat st j in dom M holds
M . j = H₁(j) from FINSEQ_2:sch 1();
A35: dom M = Seg (m -' n) by A33, FINSEQ_1:def 3;
reconsider M = M as FinSequence of the carrier of (m -VectSp_over K) by A10, MATRIX13:102;
reconsider M1 = FinS2MX M as Matrix of m -' n,m,K by A33;

now :: thesis:

let i be Nat; :: thesis:
assume A36: i in Seg (m -' n) ; :: thesis:
take a = f /. ((Sgm ((Seg m) \ N)) . i); :: thesis:
thus Line (M1,i) = M1 . i by A36, MATRIX_0:52
.= a * (Line (MV,i)) by A34, A35, A36 ; :: thesis:

end;

then consider L being Linear_Combination of lines MV such that
A37: L (#) (MX2FinS MV) = M1 by A27, MATRIX13:105, MATRIX13:108;
reconsider SumL = Sum L, f = f as Element of m -tuples_on the carrier of K by A31, FINSEQ_2:92, MATRIX13:102;

now :: thesis:

let i be Nat; :: thesis:
assume A38: i in Seg m ; :: thesis:
A39: (Seg m) \ N c= Seg m by XBOOLE_1:36;
A67: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by FINSEQ_1:def 14;

A40: now :: thesis:

per cases ;

suppose A41: i in N ; :: thesis:

consider X being Matrix of K such that
A42: X = ColVec2Mx f and
A43: len X = width A and
width X = width (ColVec2Mx ((len A) |-> (0. K))) and
A44: A * X = ColVec2Mx ((len A) |-> (0. K)) by A30;
A45: f = Col (X,1) by A6, A42, Th26;
reconsider F = f as Element of (width A) -tuples_on the carrier of K by A4, MATRIX_0:23;
A46: rng (Sgm (Seg (m -' n))) = Seg (m -' n) by FINSEQ_1:def 14;
A47: rng (Sgm N) = N by FINSEQ_1:def 14;
then consider x being object such that
A48: x in dom (Sgm N) and
A49: (Sgm N) . x = i by A41, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A48;
set L = Line (A,x);
A50: dom (mlt ((Line (A,x)),F)) = Seg m by A14, FINSEQ_2:124;
then consider mN, mSN being FinSequence of K such that
A51: mN = (mlt ((Line (A,x)),F)) * (Sgm N) and
A52: mSN = (mlt ((Line (A,x)),F)) * (Sgm ((Seg m) \ N)) and
A53: Sum (mlt ((Line (A,x)),F)) = (Sum mN) + (Sum mSN) by A2, Lm7;
A54: dom (Sgm N) = Seg (card N) by FINSEQ_3:40;
then A55: dom mN = Seg n by A1, A2, A47, A50, A51, RELAT_1:27;
Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A56: [x,x] in Indices (1. (K,n)) by A1, A54, A48, ZFMISC_1:87;
A57: (Sgm N) . x in N by A47, A48, FUNCT_1:def 3;
then A58: ( F . ((Sgm N) . x) = F /. ((Sgm N) . x) & (Line (A,x)) . ((Sgm N) . x) = A * (x,((Sgm N) . x)) ) by A2, A14, A31, A32, MATRIX_0:def 7, PARTFUN1:def 6;
A59: x = (idseq n) . x by A1, A54, A48, FINSEQ_2:49
.= (Sgm (Seg n)) . x by FINSEQ_3:48 ;

now :: thesis:

let j be Nat; :: thesis:
assume that
A60: j in dom mN and
A61: j <> x ; :: thesis:
Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A62: [x,j] in Indices (1. (K,n)) by A1, A54, A48, A55, A60, ZFMISC_1:87;
A63: (Sgm N) . j in N by A1, A47, A54, A55, A60, FUNCT_1:def 3;
then A64: ( F . ((Sgm N) . j) = F /. ((Sgm N) . j) & (Line (A,x)) . ((Sgm N) . j) = A * (x,((Sgm N) . j)) ) by A2, A14, A31, A32, MATRIX_0:def 7, PARTFUN1:def 6;
thus mN . j = (mlt ((Line (A,x)),F)) . ((Sgm N) . j) by A51, A60, FUNCT_1:12
.= (F /. ((Sgm N) . j)) * (A * (((Sgm (Seg n)) . x),((Sgm N) . j))) by A2, A14, A59, A63, A64, FVSUM_1:61
.= (F /. ((Sgm N) . j)) * ((1. (K,n)) * (x,j)) by A3, A62, MATRIX13:def 1
.= (F /. ((Sgm N) . j)) * (0. K) by A61, A62, MATRIX_1:def 3
.= 0. K ; :: thesis:

end;

then Sum mN = mN . x by A1, A54, A48, A55, MATRIX_3:12;
then A65: Sum mN = (mlt ((Line (A,x)),F)) . ((Sgm N) . x) by A1, A54, A48, A51, A55, FUNCT_1:12
.= (F /. ((Sgm N) . x)) * (A * (((Sgm (Seg n)) . x),((Sgm N) . x))) by A2, A14, A59, A57, A58, FVSUM_1:61
.= (F /. ((Sgm N) . x)) * ((1. (K,n)) * (x,x)) by A3, A56, MATRIX13:def 1
.= (F /. ((Sgm N) . x)) * (1_ K) by A56, MATRIX_1:def 3
.= F /. i by A49
.= f . i by A31, A32, A38, PARTFUN1:def 6 ;
A66: dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N)) by FINSEQ_3:40;
dom mSN = Seg (m -' n) by A24, A25, A50, A52, A66, A67, RELAT_1:27, XBOOLE_1:36;
then A68: len mSN = m -' n by FINSEQ_1:def 3;
A69: ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;
( Indices (0. (K,(len A),1)) = [:(Seg (len A)),(Seg 1):] & 1 in Seg 1 ) by A4, A15, MATRIX_0:23;
then A70: [x,1] in Indices (0. (K,(len A),1)) by A1, A15, A54, A48, ZFMISC_1:87;
then A71: 0. K = (ColVec2Mx ((len A) |-> (0. K))) * (x,1) by A69, MATRIX_3:1
.= (Line (A,x)) "*" (Col (X,1)) by A43, A44, A69, A70, MATRIX_3:def 4
.= Sum (mlt ((Line (A,x)),(Col (X,1)))) ;
reconsider mSN = mSN as Element of (m -' n) -tuples_on the carrier of K by A68, FINSEQ_2:92;
A72: width M1 = m by A5, MATRIX_0:23;

now :: thesis:

let j be Nat; :: thesis:
assume A73: j in Seg (m -' n) ; :: thesis:
A74: j = (idseq (m -' n)) . j by A73, FINSEQ_2:49
.= (Sgm (Seg (m -' n))) . j by FINSEQ_3:48 ;
A75: Line (M1,j) = M1 . j by A73, MATRIX_0:52
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (Line (MV,j)) by A34, A35, A73 ;
A76: (Sgm ((Seg m) \ N)) . j in (Seg m) \ N by A24, A25, A67, A66, A73, FUNCT_1:def 3;
then ( f /. ((Sgm ((Seg m) \ N)) . j) = F . ((Sgm ((Seg m) \ N)) . j) & A * (x,((Sgm ((Seg m) \ N)) . j)) = (Line (A,x)) . ((Sgm ((Seg m) \ N)) . j) ) by A14, A31, A32, A39, MATRIX_0:def 7, PARTFUN1:def 6;
then A77: (f /. ((Sgm ((Seg m) \ N)) . j)) * (A * (x,((Sgm ((Seg m) \ N)) . j))) = (mlt ((Line (A,x)),F)) . ((Sgm ((Seg m) \ N)) . j) by A14, A39, A76, FVSUM_1:61
.= mSN . j by A24, A25, A52, A66, A73, FUNCT_1:13 ;
A78: x = (idseq n) . x by A1, A54, A48, FINSEQ_2:49
.= (Sgm (Seg n)) . x by FINSEQ_3:48 ;
A79: [:(Seg (m -' n)),N:] c= Indices MV by A2, A12, ZFMISC_1:95;
[j,i] in Indices MV by A2, A12, A41, A73, ZFMISC_1:87;
then A80: [j,x] in Indices (Segm (MV,(Seg (m -' n)),N)) by A47, A49, A46, A74, A79, MATRIX13:17;
then A81: [j,x] in Indices ((Segm (A,(Seg n),((Seg m) \ N))) @) by A8, Lm1;
then A82: [x,j] in Indices (Segm (A,(Seg n),((Seg m) \ N))) by MATRIX_0:def 6;
A83: (Line (MV,j)) . i = MV * (((Sgm (Seg (m -' n))) . j),((Sgm N) . x)) by A10, A38, A49, A74, MATRIX_0:def 7
.= (- ((Segm (A,(Seg n),((Seg m) \ N))) @)) * (j,x) by A8, A80, MATRIX13:def 1
.= - (((Segm (A,(Seg n),((Seg m) \ N))) @) * (j,x)) by A81, MATRIX_3:def 2
.= - ((Segm (A,(Seg n),((Seg m) \ N))) * (x,j)) by A82, MATRIX_0:def 6
.= - (A * (x,((Sgm ((Seg m) \ N)) . j))) by A82, A78, MATRIX13:def 1 ;
dom M1 = Seg (m -' n) by A33, FINSEQ_1:def 3;
hence (Col (M1,i)) . j = M1 * (j,i) by A73, MATRIX_0:def 8
.= (Line (M1,j)) . i by A38, A72, MATRIX_0:def 7
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (- (A * (x,((Sgm ((Seg m) \ N)) . j)))) by A2, A10, A41, A75, A83, FVSUM_1:51
.= - ((f /. ((Sgm ((Seg m) \ N)) . j)) * (A * (x,((Sgm ((Seg m) \ N)) . j)))) by VECTSP_1:8
.= (- mSN) . j by A73, A77, FVSUM_1:23 ;
:: thesis:

end;

then Col (M1,i) = - mSN by A33, FINSEQ_2:119;
hence Sum (Col (M1,i)) = - (Sum mSN) by FVSUM_1:75
.= (- (Sum mSN)) + ((Sum mSN) + (Sum mN)) by A71, A45, A53, RLVECT_1:def 4
.= ((- (Sum mSN)) + (Sum mSN)) + (Sum mN) by RLVECT_1:def 3
.= (0. K) + (Sum mN) by VECTSP_1:19
.= f . i by A65, RLVECT_1:def 4 ;
:: thesis:

end;

suppose A84: not i in N ; :: thesis:

i in (Seg m) \ N by A38, A84, XBOOLE_0:def 5;
then consider x being object such that
A86: x in dom (Sgm ((Seg m) \ N)) and
A87: (Sgm ((Seg m) \ N)) . x = i by A67, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A86;
A88: dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N)) by FINSEQ_3:40;
then A89: Line (M1,x) = M1 . x by A24, A25, A86, MATRIX_0:52
.= (f /. ((Sgm ((Seg m) \ N)) . x)) * (Line (MV,x)) by A24, A25, A34, A35, A88, A86 ;
[x,x] in [:(Seg (m -' n)),(Seg (m -' n)):] by A24, A25, A88, A86, ZFMISC_1:87;
then A90: [x,x] in Indices (1. (K,(m -' n))) by MATRIX_0:24;
x = (idseq (m -' n)) . x by A24, A25, A88, A86, FINSEQ_2:49
.= (Sgm (Seg (m -' n))) . x by FINSEQ_3:48 ;
then A91: (Line (MV,x)) . i = MV * (((Sgm (Seg (m -' n))) . x),((Sgm ((Seg m) \ N)) . x)) by A10, A38, A87, MATRIX_0:def 7
.= (1. (K,(m -' n))) * (x,x) by A7, A90, MATRIX13:def 1
.= 1_ K by A90, MATRIX_1:def 3 ;
A92: dom (Col (M1,i)) = Seg (len M1) by FINSEQ_2:124;
A93: dom M1 = Seg (len M1) by FINSEQ_1:def 3;
A94: len M1 = m - n by A5, A24, MATRIX_0:23;
A95: width M1 = m by A5, MATRIX_0:23;

A96: now :: thesis:

let j be Nat; :: thesis:
assume that
A97: j in dom (Col (M1,i)) and
A98: x <> j ; :: thesis:
A99: Line (M1,j) = M1 . j by A92, A97, MATRIX_0:52
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (Line (MV,j)) by A34, A92, A93, A97 ;
[j,x] in [:(Seg (m -' n)),(Seg (m -' n)):] by A24, A25, A88, A86, A92, A94, A97, ZFMISC_1:87;
then A100: [j,x] in Indices (1. (K,(m -' n))) by MATRIX_0:24;
j = (idseq (m -' n)) . j by A24, A92, A94, A97, FINSEQ_2:49
.= (Sgm (Seg (m -' n))) . j by FINSEQ_3:48 ;
then A101: (Line (MV,j)) . i = MV * (((Sgm (Seg (m -' n))) . j),((Sgm ((Seg m) \ N)) . x)) by A10, A38, A87, MATRIX_0:def 7
.= (1. (K,(m -' n))) * (j,x) by A7, A100, MATRIX13:def 1
.= 0. K by A98, A100, MATRIX_1:def 3 ;
thus (Col (M1,i)) . j = M1 * (j,i) by A92, A93, A97, MATRIX_0:def 8
.= ((f /. ((Sgm ((Seg m) \ N)) . j)) * (Line (MV,j))) . i by A38, A95, A99, MATRIX_0:def 7
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (0. K) by A10, A38, A101, FVSUM_1:51
.= 0. K ; :: thesis:

end;

(Col (M1,i)) . x = M1 * (x,i) by A25, A88, A86, A94, A93, MATRIX_0:def 8
.= (Line (M1,x)) . i by A38, A95, MATRIX_0:def 7
.= (f /. ((Sgm ((Seg m) \ N)) . x)) * (1_ K) by A10, A38, A91, A89, FVSUM_1:51
.= f /. i by A87
.= f . i by A31, A32, A38, PARTFUN1:def 6 ;
hence Sum (Col (M1,i)) = f . i by A25, A88, A86, A92, A94, A96, MATRIX_3:12; :: thesis:

end;

Carrier L c= lines MV by VECTSP_6:def 4;
hence SumL . i = f . i by A27, A37, A38, A40, MATRIX13:105, MATRIX13:107; :: thesis:

end;

then A102: SumL = f by FINSEQ_2:119;
the carrier of (Lin (lines MV)) = { (Sum l) where l is Linear_Combination of lines MV : verum } by VECTSP_7:def 2;
hence y in the carrier of (Lin (lines MV)) by A29, A102; :: thesis:

end;

take MV ; :: thesis:
Solutions_of (A,((len A) |-> (0. K))) = the carrier of (Space_of_Solutions_of A) by A6, A14, Def5;
then the carrier of (Lin (lines MV)) c= the carrier of (Space_of_Solutions_of A) by A20, VECTSP_7:11;
then the carrier of (Lin (lines MV)) = the carrier of (Space_of_Solutions_of A) by A28;
hence ( Segm (MV,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MV,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MV) = Space_of_Solutions_of A ) by A14, A7, A8, VECTSP_4:29; :: thesis: