let n, m be Nat; 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; 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; 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 ; ( 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
; 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:47, 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_1:24;
A11:
( len MV = m -' n & len MV >= the_rank_of MV )
by MATRIX13:74, MATRIX_1:def 3;
A12:
Indices MV = [:(Seg (m -' n)),(Seg m):]
by A5, MATRIX_1:24;
(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:118;
A14:
width A = m
by A4, MATRIX_1:24;
A15:
len A = n
by A4, MATRIX_1:24;
lines MV c= Solutions_of A,((len A) |-> (0. K))
proof
let x be
set ;
TARSKI:def 3 ( not x in lines MV or x in Solutions_of A,((len A) |-> (0. K)) )
assume
x in lines MV
;
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_1:24
.=
len (Line MV,k)
by FINSEQ_1:def 18
;
now let i be
Nat;
( 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
;
( 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:4, 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;
verum 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;
verum
end;
then
Lin (lines MV) is Subspace of Lin (Solutions_of A,((len A) |-> (0. K)))
by A14, VECTSP_7:18;
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:78;
then A24:
m -' n = m - n
by A1, A2, NAT_1:44, XREAL_1:235;
A25:
card ((Seg m) \ N) = m - n
by A1, A2, A23, CARD_2:63;
then A26:
card (Seg (m -' n)) = card ((Seg m) \ N)
by A24, FINSEQ_1:78;
EqSegm MV,(Seg (m -' n)),((Seg m) \ N) = 1. K,(m -' n)
by A7, A24, A25, FINSEQ_1:78, 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
set ;
TARSKI:def 3 ( 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)
;
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 H1(
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 = H1(
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 let i be
Nat;
( 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)
;
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);
Line M1,i = a * (Line MV,i)thus Line M1,
i =
M1 . i
by A36, MATRIX_2:10
.=
a * (Line MV,i)
by A34, A35, A36
;
verum 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:110, MATRIX13:102;
now let i be
Nat;
( i in Seg m implies SumL . i = f . i )assume A38:
i in Seg m
;
SumL . i = f . iA39:
(Seg m) \ N c= Seg m
by XBOOLE_1:36;
A40:
now per cases
( i in N or not i in N )
;
suppose A41:
i in N
;
Sum (Col M1,i) = f . iconsider 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, A14, A42, A43, Th26;
reconsider F =
f as
Element of
(width A) -tuples_on the
carrier of
K by A4, MATRIX_1:24;
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
set such that A48:
x in dom (Sgm N)
and A49:
(Sgm N) . x = i
by A41, FUNCT_1:def 5;
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:144;
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:45;
then A55:
dom mN = Seg n
by A1, A2, A47, A50, A51, RELAT_1:46;
Indices (1. K,n) = [:(Seg n),(Seg n):]
by MATRIX_1:25;
then A56:
[x,x] in Indices (1. K,n)
by A1, A54, A48, ZFMISC_1:106;
A57:
(Sgm N) . x in N
by A47, A48, FUNCT_1:def 5;
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_1:def 8, PARTFUN1:def 8;
A59:
x =
(idseq n) . x
by A1, A54, A48, FINSEQ_2:57
.=
(Sgm (Seg n)) . x
by FINSEQ_3:54
;
now let j be
Nat;
( j in dom mN & j <> x implies mN . j = 0. K )assume that A60:
j in dom mN
and A61:
j <> x
;
mN . j = 0. K
Indices (1. K,n) = [:(Seg n),(Seg n):]
by MATRIX_1:25;
then A62:
[x,j] in Indices (1. K,n)
by A1, A54, A48, A55, A60, ZFMISC_1:106;
A63:
(Sgm N) . j in N
by A1, A47, A54, A55, A60, FUNCT_1:def 5;
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_1:def 8, PARTFUN1:def 8;
thus mN . j =
(mlt (Line A,x),F) . ((Sgm N) . j)
by A51, A60, FUNCT_1:22
.=
(F /. ((Sgm N) . j)) * (A * ((Sgm (Seg n)) . x),((Sgm N) . j))
by A2, A14, A59, A63, A64, FVSUM_1:74
.=
(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 12
.=
0. K
by VECTSP_1:36
;
verum end; then
Sum mN = mN . x
by A1, A54, A48, A55, MATRIX_3:14;
then A65:
Sum mN =
(mlt (Line A,x),F) . ((Sgm N) . x)
by A1, A54, A48, A51, A55, FUNCT_1:22
.=
(F /. ((Sgm N) . x)) * (A * ((Sgm (Seg n)) . x),((Sgm N) . x))
by A2, A14, A59, A57, A58, FVSUM_1:74
.=
(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 12
.=
F /. i
by A49, VECTSP_1:def 13
.=
f . i
by A31, A32, A38, PARTFUN1:def 8
;
A66:
dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N))
by FINSEQ_3:45, 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:46, 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_1:24;
then A70:
[x,1] in Indices (0. K,(len A),1)
by A1, A15, A54, A48, ZFMISC_1:106;
then A71:
0. K =
(ColVec2Mx ((len A) |-> (0. K))) * x,1
by A69, MATRIX_3:3
.=
(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:110;
A72:
width M1 = m
by A5, MATRIX_1:24;
now let j be
Nat;
( j in Seg (m -' n) implies (Col M1,i) . j = (- mSN) . j )assume A73:
j in Seg (m -' n)
;
(Col M1,i) . j = (- mSN) . jA74:
j =
(idseq (m -' n)) . j
by A73, FINSEQ_2:57
.=
(Sgm (Seg (m -' n))) . j
by FINSEQ_3:54
;
A75:
Line M1,
j =
M1 . j
by A73, MATRIX_2:10
.=
(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 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 A14, A31, A32, A39, MATRIX_1:def 8, PARTFUN1:def 8;
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:74
.=
mSN . j
by A24, A25, A52, A66, A73, FUNCT_1:23
;
A78:
x =
(idseq n) . x
by A1, A54, A48, FINSEQ_2:57
.=
(Sgm (Seg n)) . x
by FINSEQ_3:54
;
A79:
[:(Seg (m -' n)),N:] c= Indices MV
by A2, A12, ZFMISC_1:118;
[j,i] in Indices MV
by A2, A12, A41, A73, ZFMISC_1:106;
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_1:def 7;
A83:
(Line MV,j) . i =
MV * ((Sgm (Seg (m -' n))) . j),
((Sgm N) . x)
by A10, A38, A49, A74, MATRIX_1:def 8
.=
(- ((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_1:def 7
.=
- (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_1:def 9
.=
(Line M1,j) . i
by A38, A72, MATRIX_1:def 8
.=
(f /. ((Sgm ((Seg m) \ N)) . j)) * (- (A * x,((Sgm ((Seg m) \ N)) . j)))
by A2, A10, A41, A75, A83, FVSUM_1:63
.=
- ((f /. ((Sgm ((Seg m) \ N)) . j)) * (A * x,((Sgm ((Seg m) \ N)) . j)))
by VECTSP_1:40
.=
(- mSN) . j
by A73, A77, FVSUM_1:31
;
verum end; then
Col M1,
i = - mSN
by A33, FINSEQ_2:139;
hence Sum (Col M1,i) =
- (Sum mSN)
by FVSUM_1:94
.=
(- (Sum mSN)) + ((Sum mSN) + (Sum mN))
by A71, A45, A53, 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 A65, RLVECT_1:def 7
;
verum end; suppose A84:
not
i in N
;
Sum (Col M1,i) = f . iA85:
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
set such that A86:
x in dom (Sgm ((Seg m) \ N))
and A87:
(Sgm ((Seg m) \ N)) . x = i
by A85, FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A86;
A88:
dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N))
by FINSEQ_3:45, XBOOLE_1:36;
then A89:
Line M1,
x =
M1 . x
by A24, A25, A86, MATRIX_2:10
.=
(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:106;
then A90:
[x,x] in Indices (1. K,(m -' n))
by MATRIX_1:25;
x =
(idseq (m -' n)) . x
by A24, A25, A88, A86, FINSEQ_2:57
.=
(Sgm (Seg (m -' n))) . x
by FINSEQ_3:54
;
then A91:
(Line MV,x) . i =
MV * ((Sgm (Seg (m -' n))) . x),
((Sgm ((Seg m) \ N)) . x)
by A10, A38, A87, MATRIX_1:def 8
.=
(1. K,(m -' n)) * x,
x
by A7, A90, MATRIX13:def 1
.=
1_ K
by A90, MATRIX_1:def 12
;
A92:
dom (Col M1,i) = Seg (len M1)
by FINSEQ_2:144;
A93:
dom M1 = Seg (len M1)
by FINSEQ_1:def 3;
A94:
len M1 = m - n
by A5, A24, MATRIX_1:24;
A95:
width M1 = m
by A5, MATRIX_1:24;
A96:
now let j be
Nat;
( 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
;
(Col M1,i) . j = 0. KA99:
Line M1,
j =
M1 . j
by A92, A97, MATRIX_2:10
.=
(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:106;
then A100:
[j,x] in Indices (1. K,(m -' n))
by MATRIX_1:25;
j =
(idseq (m -' n)) . j
by A24, A92, A94, A97, FINSEQ_2:57
.=
(Sgm (Seg (m -' n))) . j
by FINSEQ_3:54
;
then A101:
(Line MV,j) . i =
MV * ((Sgm (Seg (m -' n))) . j),
((Sgm ((Seg m) \ N)) . x)
by A10, A38, A87, MATRIX_1:def 8
.=
(1. K,(m -' n)) * j,
x
by A7, A100, MATRIX13:def 1
.=
0. K
by A98, A100, MATRIX_1:def 12
;
thus (Col M1,i) . j =
M1 * j,
i
by A92, A93, A97, MATRIX_1:def 9
.=
((f /. ((Sgm ((Seg m) \ N)) . j)) * (Line MV,j)) . i
by A38, A95, A99, MATRIX_1:def 8
.=
(f /. ((Sgm ((Seg m) \ N)) . j)) * (0. K)
by A10, A38, A101, FVSUM_1:63
.=
0. K
by VECTSP_1:36
;
verum end; (Col M1,i) . x =
M1 * x,
i
by A25, A88, A86, A94, A93, MATRIX_1:def 9
.=
(Line M1,x) . i
by A38, A95, MATRIX_1:def 8
.=
(f /. ((Sgm ((Seg m) \ N)) . x)) * (1_ K)
by A10, A38, A91, A89, FVSUM_1:63
.=
f /. i
by A87, VECTSP_1:def 13
.=
f . i
by A31, A32, A38, PARTFUN1:def 8
;
hence
Sum (Col M1,i) = f . i
by A25, A88, A86, A92, A94, A96, MATRIX_3:14;
verum end;
Carrier L c= lines MV
by VECTSP_6:def 7;
hence
SumL . i = f . i
by A27, A37, A38, A40, MATRIX13:105, MATRIX13:107;
verum end;
then A102:
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 A29, A102;
verum
end;
take
MV
; ( 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 )
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:16;
then
the carrier of (Lin (lines MV)) = the carrier of (Space_of_Solutions_of A)
by A28, 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 A14, A7, A8, VECTSP_4:37; verum