let n, m 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 & N c= Seg m ) and
A2: Segm A,(Seg n),N = 1. K,n and
A3: ( n > 0 & m -' n > 0 ) ; :: thesis:
A4: m <> 0 by A1, A3, CARD_1:47, FINSEQ_1:4, XBOOLE_1:3;
then A5: ( len A = n & width A = m & m > 0 ) by A3, MATRIX_1:24;
consider MV being Matrix of m -' n,m,K such that
A6: Segm MV,(Seg (m -' n)),((Seg m) \ N) = 1. K,(m -' n) and
A7: Segm MV,(Seg (m -' n)),N = - ((Segm A,(Seg n),((Seg m) \ N)) @ ) and
A8: 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, Th49;
take MV ; :: thesis:
A9: ( len MV = m -' n & width MV = m & Indices MV = [:(Seg (m -' n)),(Seg m):] ) by A3, MATRIX_1:24;
A10: lines MV c= Solutions_of A,((len A) |-> (0. K))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: x in lines MV ; :: thesis:
consider k being Nat such that
A12: ( k in Seg (m -' n) & x = Line MV,k ) by A11, MATRIX13:103;
set C = ColVec2Mx (Line MV,k);
A13: m = width MV by A3, MATRIX_1:24
.= len (Line MV,k) by FINSEQ_1:def 18 ;

now

let i be Nat; :: thesis:
assume i in Seg 1 ; :: thesis:
then ( i = 1 & Col (ColVec2Mx (Line MV,k)),1 = Line MV,k ) by A13, A4, Th26, FINSEQ_1:4, TARSKI:def 1;
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 A12; :: thesis:

end;

then ColVec2Mx (Line MV,k) in Solutions_of A,(0. K,n,1) by A13, A8;
then ColVec2Mx (Line MV,k) in Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) by A5, Th32;
hence x in Solutions_of A,((len A) |-> (0. K)) by A12; :: thesis:

end;

A14: Solutions_of A,((len A) |-> (0. K)) = the carrier of (Space_of_Solutions_of A) by A5, Def5;
Lin (lines MV) is Subspace of Lin (Solutions_of A,((len A) |-> (0. K))) by A10, A5, VECTSP_7:18;
then the carrier of (Lin (lines MV)) c= the carrier of (Lin (Solutions_of A,((len A) |-> (0. K)))) by VECTSP_4:def 2;
then A15: the carrier of (Lin (lines MV)) c= the carrier of (Space_of_Solutions_of A) by A14, VECTSP_7:16;
( n <= card (Seg m) & card (Seg m) = m ) by A1, FINSEQ_1:78, NAT_1:44;
then A16: ( m -' n = m - n & card ((Seg m) \ N) = m - n ) by A1, CARD_2:63, XREAL_1:235;
then A17: card (Seg (m -' n)) = card ((Seg m) \ N) by FINSEQ_1:78;
A18: the_rank_of MV = m -' n

proof

A19: EqSegm MV,(Seg (m -' n)),((Seg m) \ N) = 1. K,(m -' n) by A6, A16, FINSEQ_1:78, MATRIX13:def 3;
(Seg m) \ N c= Seg m by XBOOLE_1:36;
then A20: [:(Seg (m -' n)),((Seg m) \ N):] c= Indices MV by A9, ZFMISC_1:118;
(m -' n) + 0 > 0 by A3;
then m -' n >= 1 by NAT_1:19;
then ( Det (1. K,(m -' n)) = 1_ K & 0. K <> 1_ K ) by MATRIX_7:16;
then A21: m -' n <= the_rank_of MV by A16, A17, A19, A20, MATRIX13:def 4;
( len MV = m -' n & len MV >= the_rank_of MV ) by MATRIX13:74, MATRIX_1:def 3;
hence the_rank_of MV = m -' n by A21, XXREAL_0:1; :: thesis:

end;

the carrier of (Space_of_Solutions_of A) c= the carrier of (Lin (lines MV))

proof

let y be set ; :: 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 A5, Def5;
then consider f being FinSequence of K such that
A22: ( f = y & ColVec2Mx f in Solutions_of A,(ColVec2Mx ((len A) |-> (0. K))) ) ;
A23: ( len f = m & dom f = Seg (len f) ) by A5, A22, Th59, FINSEQ_1:def 3;
set SN = (Seg m) \ N;
deffunc H₁( Nat) -> Element of (width MV) -tuples_on the carrier of K = (f /. ((Sgm ((Seg m) \ N)) . $1)) * (Line MV,$1);
consider M being FinSequence of (width MV) -tuples_on the carrier of K such that
A24: len M = m -' n and
A25: for j being Nat st j in dom M holds
M . j = H₁(j) from FINSEQ_2:sch 1();
A26: dom M = Seg (m -' n) by A24, FINSEQ_1:def 3;
reconsider M = M as FinSequence of the carrier of (m -VectSp_over K) by A9, MATRIX13:102;
reconsider M1 = FinS2MX M as Matrix of m -' n,m,K by A24;
A27: MV is one-to-one by A18, MATRIX13:105;

now

let i be Nat; :: thesis:
assume A28: i in Seg (m -' n) ; :: thesis:
take a = f /. ((Sgm ((Seg m) \ N)) . i); :: thesis:
thus Line M1,i = M1 . i by A28, MATRIX_2:10
.= a * (Line MV,i) by A28, A25, A26 ; :: thesis:

end;

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

now

let i be Nat; :: thesis:
assume A30: i in Seg m ; :: thesis:
A31: (Seg m) \ N c= Seg m by XBOOLE_1:36;

A32: now

per cases ;

suppose A33: i in N ; :: thesis:

A34: ( rng (Sgm N) = N & dom (Sgm N) = Seg (card N) ) by A1, FINSEQ_1:def 13, FINSEQ_3:45;
then consider x being set such that
A35: ( x in dom (Sgm N) & (Sgm N) . x = i ) by A33, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A35;
consider X being Matrix of K such that
A36: X = ColVec2Mx f and
A37: ( len X = width A & width X = width (ColVec2Mx ((len A) |-> (0. K))) ) and
A38: A * X = ColVec2Mx ((len A) |-> (0. K)) by A22;
A39: ( ColVec2Mx ((len A) |-> (0. K)) = 0. K,(len A),1 & Indices (0. K,(len A),1) = [:(Seg (len A)),(Seg 1):] & 1 in Seg 1 ) by Th32, A5, A3, MATRIX_1:24;
then A40: [x,1] in Indices (0. K,(len A),1) by A1, A34, A35, A5, ZFMISC_1:106;
then A41: 0. K = (ColVec2Mx ((len A) |-> (0. K))) * x,1 by A39, MATRIX_3:3
.= (Line A,x) "*" (Col X,1) by A37, A38, A40, A39, MATRIX_3:def 4
.= Sum (mlt (Line A,x),(Col X,1)) ;
A42: f = Col X,1 by A5, A37, A36, Th26;
reconsider F = f as Element of (width A) -tuples_on the carrier of K by A3, MATRIX_1:24;
set L = Line A,x;
A43: dom (mlt (Line A,x),F) = Seg m by A5, FINSEQ_2:144;
then consider mN, mSN being FinSequence of K such that
A44: mN = (mlt (Line A,x),F) * (Sgm N) and
A45: mSN = (mlt (Line A,x),F) * (Sgm ((Seg m) \ N)) and
A46: Sum (mlt (Line A,x),F) = (Sum mN) + (Sum mSN) by A1, Lm7;
A47: ( rng (Sgm (Seg (m -' n))) = Seg (m -' n) & rng (Sgm ((Seg m) \ N)) = (Seg m) \ N & dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N)) ) by A31, FINSEQ_1:def 13, FINSEQ_3:45;
then A48: ( dom mN = Seg n & dom mSN = Seg (m -' n) ) by A1, A43, A44, A45, A34, A16, RELAT_1:46, XBOOLE_1:36;
then len mSN = m -' n by FINSEQ_1:def 3;
then reconsider mSN = mSN as Element of (m -' n) -tuples_on the carrier of K by FINSEQ_2:110;
A49: width M1 = m by A3, MATRIX_1:24;
A50: x = (idseq n) . x by A1, A35, A34, FINSEQ_2:57
.= (Sgm (Seg n)) . x by FINSEQ_3:54 ;

now

let j be Nat; :: thesis:
assume A51: ( j in dom mN & j <> x ) ; :: thesis:
A52: (Sgm N) . j in N by A51, A48, A1, A34, FUNCT_1:def 5;
then A53: ( F . ((Sgm N) . j) = F /. ((Sgm N) . j) & (Line A,x) . ((Sgm N) . j) = A * x,((Sgm N) . j) ) by A1, A23, A5, MATRIX_1:def 8, PARTFUN1:def 8;
Indices (1. K,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A54: [x,j] in Indices (1. K,n) by A51, A1, A35, A48, A34, ZFMISC_1:106;
thus mN . j = (mlt (Line A,x),F) . ((Sgm N) . j) by A51, A44, FUNCT_1:22
.= (F /. ((Sgm N) . j)) * (A * ((Sgm (Seg n)) . x),((Sgm N) . j)) by A52, A50, A1, A5, A53, FVSUM_1:74
.= (F /. ((Sgm N) . j)) * ((1. K,n) * x,j) by A54, A2, MATRIX13:def 1
.= (F /. ((Sgm N) . j)) * (0. K) by A54, A51, MATRIX_1:def 12
.= 0. K by VECTSP_1:36 ; :: thesis:

end;

then A55: Sum mN = mN . x by A1, A35, A48, A34, MATRIX_3:14;
A56: (Sgm N) . x in N by A35, A34, FUNCT_1:def 5;
then A57: ( F . ((Sgm N) . x) = F /. ((Sgm N) . x) & (Line A,x) . ((Sgm N) . x) = A * x,((Sgm N) . x) ) by A1, A23, A5, MATRIX_1:def 8, PARTFUN1:def 8;
Indices (1. K,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A58: [x,x] in Indices (1. K,n) by A34, A35, A1, ZFMISC_1:106;
A59: Sum mN = (mlt (Line A,x),F) . ((Sgm N) . x) by A55, A44, A1, A35, A48, A34, FUNCT_1:22
.= (F /. ((Sgm N) . x)) * (A * ((Sgm (Seg n)) . x),((Sgm N) . x)) by A56, A50, A1, A5, A57, FVSUM_1:74
.= (F /. ((Sgm N) . x)) * ((1. K,n) * x,x) by A58, A2, MATRIX13:def 1
.= (F /. ((Sgm N) . x)) * (1_ K) by A58, MATRIX_1:def 12
.= F /. i by A35, VECTSP_1:def 13
.= f . i by A30, A23, PARTFUN1:def 8 ;

now

let j be Nat; :: thesis:
assume A60: j in Seg (m -' n) ; :: thesis:
A61: Line M1,j = M1 . j by A60, MATRIX_2:10
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (Line MV,j) by A25, A60, A26 ;
A62: j = (idseq (m -' n)) . j by A60, FINSEQ_2:57
.= (Sgm (Seg (m -' n))) . j by FINSEQ_3:54 ;
( [:(Seg (m -' n)),N:] c= Indices MV & [j,i] in Indices MV ) by A9, A1, A60, A33, ZFMISC_1:106, ZFMISC_1:118;
then A63: [j,x] in Indices (Segm MV,(Seg (m -' n)),N) by A62, A47, A35, A34, MATRIX13:17;
then A64: [j,x] in Indices ((Segm A,(Seg n),((Seg m) \ N)) @ ) by A7, Lm1;
then A65: [x,j] in Indices (Segm A,(Seg n),((Seg m) \ N)) by MATRIX_1:def 7;
A66: x = (idseq n) . x by A35, A34, A1, FINSEQ_2:57
.= (Sgm (Seg n)) . x by FINSEQ_3:54 ;
A67: (Line MV,j) . i = MV * ((Sgm (Seg (m -' n))) . j),((Sgm N) . x) by A9, A35, A62, A30, MATRIX_1:def 8
.= (- ((Segm A,(Seg n),((Seg m) \ N)) @ )) * j,x by A63, A7, MATRIX13:def 1
.= - (((Segm A,(Seg n),((Seg m) \ N)) @ ) * j,x) by A64, MATRIX_3:def 2
.= - ((Segm A,(Seg n),((Seg m) \ N)) * x,j) by A65, MATRIX_1:def 7
.= - (A * x,((Sgm ((Seg m) \ N)) . j)) by A65, A66, MATRIX13:def 1 ;
A68: (Sgm ((Seg m) \ N)) . j in (Seg m) \ N by A16, A47, A60, FUNCT_1:def 5;
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 A23, A5, A31, MATRIX_1:def 8, PARTFUN1:def 8;
then A69: (f /. ((Sgm ((Seg m) \ N)) . j)) * (A * x,((Sgm ((Seg m) \ N)) . j)) = (mlt (Line A,x),F) . ((Sgm ((Seg m) \ N)) . j) by A5, A68, A31, FVSUM_1:74
.= mSN . j by A45, A16, A47, A60, FUNCT_1:23 ;
dom M1 = Seg (m -' n) by A24, FINSEQ_1:def 3;
hence (Col M1,i) . j = M1 * j,i by A60, MATRIX_1:def 9
.= (Line M1,j) . i by A49, A30, MATRIX_1:def 8
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (- (A * x,((Sgm ((Seg m) \ N)) . j))) by A61, A9, A33, A1, A67, FVSUM_1:63
.= - ((f /. ((Sgm ((Seg m) \ N)) . j)) * (A * x,((Sgm ((Seg m) \ N)) . j))) by VECTSP_1:40
.= (- mSN) . j by A60, A69, FVSUM_1:31 ;
:: thesis:

end;

then Col M1,i = - mSN by A24, FINSEQ_2:139;
hence Sum (Col M1,i) = - (Sum mSN) by FVSUM_1:94
.= (- (Sum mSN)) + ((Sum mSN) + (Sum mN)) by A46, A41, A42, RLVECT_1:def 7
.= ((- (Sum mSN)) + (Sum mSN)) + (Sum mN) by RLVECT_1:def 6
.= (0. K) + (Sum mN) by VECTSP_1:66
.= f . i by A59, RLVECT_1:def 7 ;
:: thesis:

end;

suppose not i in N ; :: thesis:

then A70: ( i in (Seg m) \ N & rng (Sgm ((Seg m) \ N)) = (Seg m) \ N & dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N)) ) by A30, A31, FINSEQ_1:def 13, FINSEQ_3:45, XBOOLE_0:def 5;
then consider x being set such that
A71: ( x in dom (Sgm ((Seg m) \ N)) & (Sgm ((Seg m) \ N)) . x = i ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A71;
A72: ( dom (Col M1,i) = Seg (len M1) & len M1 = m - n & width M1 = m & dom M1 = Seg (len M1) ) by A3, A16, FINSEQ_1:def 3, FINSEQ_2:144, MATRIX_1:24;

A73: now

let j be Nat; :: thesis:
assume A74: ( j in dom (Col M1,i) & x <> j ) ; :: thesis:
[j,x] in [:(Seg (m -' n)),(Seg (m -' n)):] by A70, A71, A72, A74, A16, ZFMISC_1:106;
then A75: [j,x] in Indices (1. K,(m -' n)) by MATRIX_1:25;
j = (idseq (m -' n)) . j by A72, A74, A16, FINSEQ_2:57
.= (Sgm (Seg (m -' n))) . j by FINSEQ_3:54 ;
then A76: (Line MV,j) . i = MV * ((Sgm (Seg (m -' n))) . j),((Sgm ((Seg m) \ N)) . x) by A9, A71, A30, MATRIX_1:def 8
.= (1. K,(m -' n)) * j,x by A75, A6, MATRIX13:def 1
.= 0. K by A75, A74, MATRIX_1:def 12 ;
A77: Line M1,j = M1 . j by A72, A74, MATRIX_2:10
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (Line MV,j) by A25, A74, A72 ;
thus (Col M1,i) . j = M1 * j,i by A74, A72, MATRIX_1:def 9
.= ((f /. ((Sgm ((Seg m) \ N)) . j)) * (Line MV,j)) . i by A77, A30, A72, MATRIX_1:def 8
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (0. K) by A76, A30, A9, FVSUM_1:63
.= 0. K by VECTSP_1:36 ; :: thesis:

end;

[x,x] in [:(Seg (m -' n)),(Seg (m -' n)):] by A70, A71, A16, ZFMISC_1:106;
then A78: [x,x] in Indices (1. K,(m -' n)) by MATRIX_1:25;
x = (idseq (m -' n)) . x by A70, A71, A16, FINSEQ_2:57
.= (Sgm (Seg (m -' n))) . x by FINSEQ_3:54 ;
then A79: (Line MV,x) . i = MV * ((Sgm (Seg (m -' n))) . x),((Sgm ((Seg m) \ N)) . x) by A9, A71, A30, MATRIX_1:def 8
.= (1. K,(m -' n)) * x,x by A78, A6, MATRIX13:def 1
.= 1_ K by A78, MATRIX_1:def 12 ;
A80: Line M1,x = M1 . x by A70, A71, A16, MATRIX_2:10
.= (f /. ((Sgm ((Seg m) \ N)) . x)) * (Line MV,x) by A25, A70, A71, A16, A26 ;
(Col M1,i) . x = M1 * x,i by A16, A70, A71, A72, MATRIX_1:def 9
.= (Line M1,x) . i by A30, A72, MATRIX_1:def 8
.= (f /. ((Sgm ((Seg m) \ N)) . x)) * (1_ K) by A79, A30, A80, A9, FVSUM_1:63
.= f /. i by A71, VECTSP_1:def 13
.= f . i by A23, A30, PARTFUN1:def 8 ;
hence Sum (Col M1,i) = f . i by A73, A72, A70, A71, A16, MATRIX_3:14; :: thesis:

end;

Carrier L c= lines MV by VECTSP_6:def 7;
hence SumL . i = f . i by A32, A30, A29, A18, MATRIX13:105, MATRIX13:107; :: thesis:

end;

then A81: SumL = f by FINSEQ_2:139;
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 A81, A22; :: thesis:

end;

then the carrier of (Lin (lines MV)) = the carrier of (Space_of_Solutions_of A) by A15, XBOOLE_0:def 10;
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 A6, A7, A5, VECTSP_4:37; :: thesis: