let m, n be Nat; :: thesis: for K being Field

for A being Matrix of n,m,K

for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )

let K be Field; :: thesis: for A being Matrix of n,m,K

for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )

let A be Matrix of n,m,K; :: thesis: for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )

let N be finite without_zero Subset of NAT; :: thesis: ( card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 implies ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A ) )

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: ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )

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)))

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))

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: verum

for A being Matrix of n,m,K

for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )

let K be Field; :: thesis: for A being Matrix of n,m,K

for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )

let A be Matrix of n,m,K; :: thesis: for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )

let N be finite without_zero Subset of NAT; :: thesis: ( card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 implies ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A ) )

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: ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )

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

then
Lin (lines MV) is Subspace of Lin (Solutions_of (A,((len A) |-> (0. K))))
by A14, VECTSP_7:13;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lines MV or x in Solutions_of (A,((len A) |-> (0. K))) )

assume x in lines MV ; :: thesis: x in Solutions_of (A,((len A) |-> (0. K)))

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 ;

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: verum

end;assume x in lines MV ; :: thesis: x in Solutions_of (A,((len A) |-> (0. K)))

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: for i being Nat holds

( not i in Seg 1 or 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) )

then
ColVec2Mx (Line (MV,k)) in Solutions_of (A,(0. (K,n,1)))
by A9, A18;( not i in Seg 1 or 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) )

let i be Nat; :: thesis: ( not i in Seg 1 or 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) )

assume i in Seg 1 ; :: thesis: ( 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) )

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: verum

end;( j in Seg (m -' n) & Col ((ColVec2Mx (Line (MV,k))),i) = Line (MV,j) ) or Col ((ColVec2Mx (Line (MV,k))),i) = m |-> (0. K) )

assume i in Seg 1 ; :: thesis: ( 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) )

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: verum

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: verum

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

take
MV
; :: thesis: ( 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 )
set SN = (Seg m) \ N;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (Space_of_Solutions_of A) or y in the carrier of (Lin (lines MV)) )

assume y in the carrier of (Space_of_Solutions_of A) ; :: thesis: y in the carrier of (Lin (lines MV))

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_{1}( 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_{1}(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;

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;

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: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (Space_of_Solutions_of A) or y in the carrier of (Lin (lines MV)) )

assume y in the carrier of (Space_of_Solutions_of A) ; :: thesis: y in the carrier of (Lin (lines MV))

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

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

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: for i being Nat st i in Seg (m -' n) holds

ex a being Element of the carrier of K st Line (M1,i) = a * (Line (MV,i))

then consider L being Linear_Combination of lines MV such that ex a being Element of the carrier of K st Line (M1,i) = a * (Line (MV,i))

let i be Nat; :: thesis: ( i in Seg (m -' n) implies ex a being Element of the carrier of K st Line (M1,i) = a * (Line (MV,i)) )

assume A36: i in Seg (m -' n) ; :: thesis: ex a being Element of the carrier of K st Line (M1,i) = a * (Line (MV,i))

take a = f /. ((Sgm ((Seg m) \ N)) . i); :: thesis: Line (M1,i) = a * (Line (MV,i))

thus Line (M1,i) = M1 . i by A36, MATRIX_0:52

.= a * (Line (MV,i)) by A34, A35, A36 ; :: thesis: verum

end;assume A36: i in Seg (m -' n) ; :: thesis: ex a being Element of the carrier of K st Line (M1,i) = a * (Line (MV,i))

take a = f /. ((Sgm ((Seg m) \ N)) . i); :: thesis: Line (M1,i) = a * (Line (MV,i))

thus Line (M1,i) = M1 . i by A36, MATRIX_0:52

.= a * (Line (MV,i)) by A34, A35, A36 ; :: thesis: verum

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: for i being Nat st i in Seg m holds

SumL . i = f . i

then A102:
SumL = f
by FINSEQ_2:119;SumL . i = f . i

let i be Nat; :: thesis: ( i in Seg m implies SumL . i = f . i )

assume A38: i in Seg m ; :: thesis: SumL . i = f . i

A39: (Seg m) \ N c= Seg m by XBOOLE_1:36;

hence SumL . i = f . i by A27, A37, A38, A40, MATRIX13:105, MATRIX13:107; :: thesis: verum

end;assume A38: i in Seg m ; :: thesis: SumL . i = f . i

A39: (Seg m) \ N c= Seg m by XBOOLE_1:36;

A40: now :: thesis: Sum (Col (M1,i)) = f . iend;

Carrier L c= lines MV
by VECTSP_6:def 4;per cases
( i in N or not i in N )
;

end;

suppose A41:
i in N
; :: thesis: Sum (Col (M1,i)) = f . i

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 13;

A47: rng (Sgm N) = N by A2, FINSEQ_1:def 13;

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 A2, 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 ;

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, XBOOLE_1:36;

A67: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by A39, FINSEQ_1:def 13;

then dom mSN = Seg (m -' n) by A24, A25, A50, A52, A66, 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;

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: verum

end;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 13;

A47: rng (Sgm N) = N by A2, FINSEQ_1:def 13;

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 A2, 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: for j being Nat st j in dom mN & j <> x holds

mN . j = 0. K

then
Sum mN = mN . x
by A1, A54, A48, A55, MATRIX_3:12;mN . j = 0. K

let j be Nat; :: thesis: ( j in dom mN & j <> x implies mN . j = 0. K )

assume that

A60: j in dom mN and

A61: j <> x ; :: thesis: mN . j = 0. K

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: verum

end;assume that

A60: j in dom mN and

A61: j <> x ; :: thesis: mN . j = 0. K

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: verum

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, XBOOLE_1:36;

A67: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by A39, FINSEQ_1:def 13;

then dom mSN = Seg (m -' n) by A24, A25, A50, A52, A66, 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: for j being Nat st j in Seg (m -' n) holds

(Col (M1,i)) . j = (- mSN) . j

then
Col (M1,i) = - mSN
by A33, FINSEQ_2:119;(Col (M1,i)) . j = (- mSN) . j

let j be Nat; :: thesis: ( j in Seg (m -' n) implies (Col (M1,i)) . j = (- mSN) . j )

assume A73: j in Seg (m -' n) ; :: thesis: (Col (M1,i)) . j = (- mSN) . j

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: verum

end;assume A73: j in Seg (m -' n) ; :: thesis: (Col (M1,i)) . j = (- mSN) . j

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: verum

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: verum

suppose A84:
not i in N
; :: thesis: Sum (Col (M1,i)) = f . i

A85:
rng (Sgm ((Seg m) \ N)) = (Seg m) \ N
by A39, FINSEQ_1:def 13;

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 A85, 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, XBOOLE_1:36;

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;

.= (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: verum

end;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 A85, 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, XBOOLE_1:36;

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: for j being Nat st j in dom (Col (M1,i)) & x <> j holds

(Col (M1,i)) . j = 0. K

(Col (M1,i)) . x =
M1 * (x,i)
by A25, A88, A86, A94, A93, MATRIX_0:def 8
(Col (M1,i)) . j = 0. K

let j be Nat; :: thesis: ( j in dom (Col (M1,i)) & x <> j implies (Col (M1,i)) . j = 0. K )

assume that

A97: j in dom (Col (M1,i)) and

A98: x <> j ; :: thesis: (Col (M1,i)) . j = 0. K

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: verum

end;assume that

A97: j in dom (Col (M1,i)) and

A98: x <> j ; :: thesis: (Col (M1,i)) . j = 0. K

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: verum

.= (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: verum

hence SumL . i = f . i by A27, A37, A38, A40, MATRIX13:105, MATRIX13:107; :: thesis: verum

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: verum

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: verum