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

for W being strict Subspace of m -VectSp_over K st dim W < m holds

ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

let K be Field; :: thesis: for W being strict Subspace of m -VectSp_over K st dim W < m holds

ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

let W be strict Subspace of m -VectSp_over K; :: thesis: ( dim W < m implies ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A ) )

assume A1: dim W < m ; :: thesis: ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

for W being strict Subspace of m -VectSp_over K st dim W < m holds

ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

let K be Field; :: thesis: for W being strict Subspace of m -VectSp_over K st dim W < m holds

ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

let W be strict Subspace of m -VectSp_over K; :: thesis: ( dim W < m implies ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A ) )

assume A1: dim W < m ; :: thesis: ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

per cases
( dim W = 0 or dim W > 0 )
;

end;

suppose A2:
dim W = 0
; :: thesis: ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

then
m -' (dim W) = m
by NAT_D:40;

then reconsider ONE = 1. (K,m) as Matrix of m -' (dim W),m,K ;

take ONE ; :: thesis: ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (ONE,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of ONE )

take Seg m ; :: thesis: ( card (Seg m) = m -' (dim W) & Seg m c= Seg m & Segm (ONE,(Seg (m -' (dim W))),(Seg m)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of ONE )

A3: len (1. (K,m)) = m by MATRIX_0:24;

A4: dim (Space_of_Solutions_of ONE) = 0 by Lm8;

A5: m -' (dim W) = m by A2, NAT_D:40;

A6: width (1. (K,m)) = m by MATRIX_0:24;

Space_of_Solutions_of ONE = (Omega). (Space_of_Solutions_of ONE)

.= (0). (Space_of_Solutions_of ONE) by A4, VECTSP_9:29

.= (0). W by A6, VECTSP_4:37

.= (Omega). W by A2, VECTSP_9:29

.= W ;

hence ( card (Seg m) = m -' (dim W) & Seg m c= Seg m & Segm (ONE,(Seg (m -' (dim W))),(Seg m)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of ONE ) by A5, A3, A6, FINSEQ_1:57, MATRIX13:46; :: thesis: verum

end;then reconsider ONE = 1. (K,m) as Matrix of m -' (dim W),m,K ;

take ONE ; :: thesis: ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (ONE,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of ONE )

take Seg m ; :: thesis: ( card (Seg m) = m -' (dim W) & Seg m c= Seg m & Segm (ONE,(Seg (m -' (dim W))),(Seg m)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of ONE )

A3: len (1. (K,m)) = m by MATRIX_0:24;

A4: dim (Space_of_Solutions_of ONE) = 0 by Lm8;

A5: m -' (dim W) = m by A2, NAT_D:40;

A6: width (1. (K,m)) = m by MATRIX_0:24;

Space_of_Solutions_of ONE = (Omega). (Space_of_Solutions_of ONE)

.= (0). (Space_of_Solutions_of ONE) by A4, VECTSP_9:29

.= (0). W by A6, VECTSP_4:37

.= (Omega). W by A2, VECTSP_9:29

.= W ;

hence ( card (Seg m) = m -' (dim W) & Seg m c= Seg m & Segm (ONE,(Seg (m -' (dim W))),(Seg m)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of ONE ) by A5, A3, A6, FINSEQ_1:57, MATRIX13:46; :: thesis: verum

suppose A7:
dim W > 0
; :: thesis: ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

( card N = m -' (dim W) & N c= Seg m & Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of A )

set ZERO = 0. (K,(m -' (dim W)),m);

A8: m - (dim W) > (dim W) - (dim W) by A1, XREAL_1:9;

A9: m -' (dim W) = m - (dim W) by A1, XREAL_1:233;

then A10: ( len (0. (K,(m -' (dim W)),m)) = m -' (dim W) & width (0. (K,(m -' (dim W)),m)) = m ) by A8, MATRIX_0:23;

A11: card (Seg m) = m by FINSEQ_1:57;

consider A being Matrix of dim W,m,K, N being finite without_zero Subset of NAT such that

A12: N c= Seg m and

A13: dim W = card N and

A14: Segm (A,(Seg (dim W)),N) = 1. (K,(dim W)) and

the_rank_of A = dim W and

A15: lines A is Basis of W by Th70;

set SA = Segm (A,(Seg (dim W)),((Seg m) \ N));

A16: card ((Seg m) \ N) = (card (Seg m)) - (card N) by A12, CARD_2:44;

then A17: width (Segm (A,(Seg (dim W)),((Seg m) \ N))) = m - (card N) by A7, A11, MATRIX_0:23;

A18: card (Seg (dim W)) = dim W by FINSEQ_1:57;

then len (Segm (A,(Seg (dim W)),((Seg m) \ N))) = dim W by A7, MATRIX_0:23;

then width ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) = dim W by A13, A8, A17, MATRIX_0:54;

then A19: width (- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)) = dim W by MATRIX_3:def 2;

A20: card (Seg (m -' (dim W))) = m -' (dim W) by FINSEQ_1:57;

m -' (dim W) = m - (dim W) by A1, XREAL_1:233;

then reconsider CC = 1. (K,(m -' (dim W))) as Matrix of card (Seg (m -' (dim W))), card ((Seg m) \ N),K by A13, A16, A11, A20;

A21: ( (Seg m) \ ((Seg m) \ N) = (Seg m) /\ N & m -' (m -' (dim W)) = m - (m -' (dim W)) ) by NAT_D:35, XBOOLE_1:48, XREAL_1:233;

A22: Indices (0. (K,(m -' (dim W)),m)) = [:(Seg (m -' (dim W))),(Seg m):] by A9, A8, MATRIX_0:23;

then A23: [:(Seg (m -' (dim W))),N:] c= Indices (0. (K,(m -' (dim W)),m)) by A12, ZFMISC_1:95;

len ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) = m - (dim W) by A13, A8, A17, MATRIX_0:54;

then len (- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)) = m -' (dim W) by A9, MATRIX_3:def 2;

then reconsider BB = - ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) as Matrix of card (Seg (m -' (dim W))), card N,K by A13, A20, A19, MATRIX_0:51;

A24: N misses (Seg m) \ N by XBOOLE_1:79;

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

then A26: [:(Seg (m -' (dim W))),((Seg m) \ N):] c= Indices (0. (K,(m -' (dim W)),m)) by A22, ZFMISC_1:95;

[:(Seg (m -' (dim W))),N:] /\ [:(Seg (m -' (dim W))),((Seg m) \ N):] = [:(Seg (m -' (dim W))),(N /\ ((Seg m) \ N)):] by ZFMISC_1:99

.= [:(Seg (m -' (dim W))),{}:] by A24

.= {} by ZFMISC_1:90 ;

then for i, j, bi, bj, ci, cj being Nat st [i,j] in [:(Seg (m -' (dim W))),N:] /\ [:(Seg (m -' (dim W))),((Seg m) \ N):] & bi = ((Sgm (Seg (m -' (dim W)))) ") . i & bj = ((Sgm N) ") . j & ci = ((Sgm (Seg (m -' (dim W)))) ") . i & cj = ((Sgm ((Seg m) \ N)) ") . j holds

BB * (bi,bj) = CC * (ci,cj) ;

then consider M being Matrix of m -' (dim W),m,K such that

A27: Segm (M,(Seg (m -' (dim W))),N) = BB and

A28: Segm (M,(Seg (m -' (dim W))),((Seg m) \ N)) = CC and

for i, j being Nat st [i,j] in (Indices M) \ ([:(Seg (m -' (dim W))),N:] \/ [:(Seg (m -' (dim W))),((Seg m) \ N):]) holds

M * (i,j) = (0. (K,(m -' (dim W)),m)) * (i,j) by A10, A23, A26, Th9;

(Seg m) /\ N = N by A12, XBOOLE_1:28;

then consider MV being Matrix of dim W,m,K such that

A29: Segm (MV,(Seg (dim W)),N) = 1. (K,(dim W)) and

A30: Segm (MV,(Seg (dim W)),((Seg m) \ N)) = - ((Segm (M,(Seg (m -' (dim W))),N)) @) and

A31: Lin (lines MV) = Space_of_Solutions_of M by A7, A13, A9, A8, A16, A11, A28, A21, Th67, XBOOLE_1:36;

take M ; :: thesis: ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (M,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of M )

take (Seg m) \ N ; :: thesis: ( card ((Seg m) \ N) = m -' (dim W) & (Seg m) \ N c= Seg m & Segm (M,(Seg (m -' (dim W))),((Seg m) \ N)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of M )

MV = A by A32, MATRIX_0:27;

then Lin lA = ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) by A15, VECTSP_7:def 3;

hence ( card ((Seg m) \ N) = m -' (dim W) & (Seg m) \ N c= Seg m & Segm (M,(Seg (m -' (dim W))),((Seg m) \ N)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of M ) by A1, A13, A16, A11, A28, A31, VECTSP_9:17, XBOOLE_1:36, XREAL_1:233; :: thesis: verum

end;A8: m - (dim W) > (dim W) - (dim W) by A1, XREAL_1:9;

A9: m -' (dim W) = m - (dim W) by A1, XREAL_1:233;

then A10: ( len (0. (K,(m -' (dim W)),m)) = m -' (dim W) & width (0. (K,(m -' (dim W)),m)) = m ) by A8, MATRIX_0:23;

A11: card (Seg m) = m by FINSEQ_1:57;

consider A being Matrix of dim W,m,K, N being finite without_zero Subset of NAT such that

A12: N c= Seg m and

A13: dim W = card N and

A14: Segm (A,(Seg (dim W)),N) = 1. (K,(dim W)) and

the_rank_of A = dim W and

A15: lines A is Basis of W by Th70;

set SA = Segm (A,(Seg (dim W)),((Seg m) \ N));

A16: card ((Seg m) \ N) = (card (Seg m)) - (card N) by A12, CARD_2:44;

then A17: width (Segm (A,(Seg (dim W)),((Seg m) \ N))) = m - (card N) by A7, A11, MATRIX_0:23;

A18: card (Seg (dim W)) = dim W by FINSEQ_1:57;

then len (Segm (A,(Seg (dim W)),((Seg m) \ N))) = dim W by A7, MATRIX_0:23;

then width ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) = dim W by A13, A8, A17, MATRIX_0:54;

then A19: width (- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)) = dim W by MATRIX_3:def 2;

A20: card (Seg (m -' (dim W))) = m -' (dim W) by FINSEQ_1:57;

m -' (dim W) = m - (dim W) by A1, XREAL_1:233;

then reconsider CC = 1. (K,(m -' (dim W))) as Matrix of card (Seg (m -' (dim W))), card ((Seg m) \ N),K by A13, A16, A11, A20;

A21: ( (Seg m) \ ((Seg m) \ N) = (Seg m) /\ N & m -' (m -' (dim W)) = m - (m -' (dim W)) ) by NAT_D:35, XBOOLE_1:48, XREAL_1:233;

A22: Indices (0. (K,(m -' (dim W)),m)) = [:(Seg (m -' (dim W))),(Seg m):] by A9, A8, MATRIX_0:23;

then A23: [:(Seg (m -' (dim W))),N:] c= Indices (0. (K,(m -' (dim W)),m)) by A12, ZFMISC_1:95;

len ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) = m - (dim W) by A13, A8, A17, MATRIX_0:54;

then len (- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)) = m -' (dim W) by A9, MATRIX_3:def 2;

then reconsider BB = - ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) as Matrix of card (Seg (m -' (dim W))), card N,K by A13, A20, A19, MATRIX_0:51;

A24: N misses (Seg m) \ N by XBOOLE_1:79;

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

then A26: [:(Seg (m -' (dim W))),((Seg m) \ N):] c= Indices (0. (K,(m -' (dim W)),m)) by A22, ZFMISC_1:95;

[:(Seg (m -' (dim W))),N:] /\ [:(Seg (m -' (dim W))),((Seg m) \ N):] = [:(Seg (m -' (dim W))),(N /\ ((Seg m) \ N)):] by ZFMISC_1:99

.= [:(Seg (m -' (dim W))),{}:] by A24

.= {} by ZFMISC_1:90 ;

then for i, j, bi, bj, ci, cj being Nat st [i,j] in [:(Seg (m -' (dim W))),N:] /\ [:(Seg (m -' (dim W))),((Seg m) \ N):] & bi = ((Sgm (Seg (m -' (dim W)))) ") . i & bj = ((Sgm N) ") . j & ci = ((Sgm (Seg (m -' (dim W)))) ") . i & cj = ((Sgm ((Seg m) \ N)) ") . j holds

BB * (bi,bj) = CC * (ci,cj) ;

then consider M being Matrix of m -' (dim W),m,K such that

A27: Segm (M,(Seg (m -' (dim W))),N) = BB and

A28: Segm (M,(Seg (m -' (dim W))),((Seg m) \ N)) = CC and

for i, j being Nat st [i,j] in (Indices M) \ ([:(Seg (m -' (dim W))),N:] \/ [:(Seg (m -' (dim W))),((Seg m) \ N):]) holds

M * (i,j) = (0. (K,(m -' (dim W)),m)) * (i,j) by A10, A23, A26, Th9;

(Seg m) /\ N = N by A12, XBOOLE_1:28;

then consider MV being Matrix of dim W,m,K such that

A29: Segm (MV,(Seg (dim W)),N) = 1. (K,(dim W)) and

A30: Segm (MV,(Seg (dim W)),((Seg m) \ N)) = - ((Segm (M,(Seg (m -' (dim W))),N)) @) and

A31: Lin (lines MV) = Space_of_Solutions_of M by A7, A13, A9, A8, A16, A11, A28, A21, Th67, XBOOLE_1:36;

A32: now :: thesis: for i, j being Nat st [i,j] in Indices A holds

A * (i,j) = MV * (i,j)

then reconsider lA = lines MV as Subset of W by A15, MATRIX_0:27;A * (i,j) = MV * (i,j)

A33:
Indices A = [:(Seg (dim W)),(Seg m):]
by A7, MATRIX_0:23;

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = MV * (i,j) )

assume A34: [i,j] in Indices A ; :: thesis: A * (i,j) = MV * (i,j)

A35: i in Seg (dim W) by A34, A33, ZFMISC_1:87;

A36: Indices A = Indices MV by MATRIX_0:26;

A37: rng (Sgm (Seg (dim W))) = Seg (dim W) by FINSEQ_1:def 13;

dom (Sgm (Seg (dim W))) = Seg (dim W) by A18, FINSEQ_3:40;

then consider x being object such that

A38: x in Seg (dim W) and

A39: (Sgm (Seg (dim W))) . x = i by A35, A37, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A38;

A40: j in Seg m by A34, A33, ZFMISC_1:87;

end;let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = MV * (i,j) )

assume A34: [i,j] in Indices A ; :: thesis: A * (i,j) = MV * (i,j)

A35: i in Seg (dim W) by A34, A33, ZFMISC_1:87;

A36: Indices A = Indices MV by MATRIX_0:26;

A37: rng (Sgm (Seg (dim W))) = Seg (dim W) by FINSEQ_1:def 13;

dom (Sgm (Seg (dim W))) = Seg (dim W) by A18, FINSEQ_3:40;

then consider x being object such that

A38: x in Seg (dim W) and

A39: (Sgm (Seg (dim W))) . x = i by A35, A37, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A38;

A40: j in Seg m by A34, A33, ZFMISC_1:87;

now :: thesis: A * (i,j) = MV * (i,j)end;

hence
A * (i,j) = MV * (i,j)
; :: thesis: verumper cases
( j in N or not j in N )
;

end;

suppose A41:
j in N
; :: thesis: A * (i,j) = MV * (i,j)

then A42:
[i,j] in [:(Seg (dim W)),N:]
by A35, ZFMISC_1:87;

A43: rng (Sgm N) = N by A12, FINSEQ_1:def 13;

dom (Sgm N) = Seg (dim W) by A12, A13, FINSEQ_3:40;

then consider y being object such that

A44: y in Seg (dim W) and

A45: (Sgm N) . y = j by A41, A43, FUNCT_1:def 3;

reconsider y = y as Element of NAT by A44;

A46: [:(Seg (dim W)),N:] c= Indices A by A12, A33, ZFMISC_1:95;

then A47: [x,y] in Indices (Segm (MV,(Seg (dim W)),N)) by A36, A37, A39, A43, A45, A42, MATRIX13:17;

[x,y] in Indices (Segm (A,(Seg (dim W)),N)) by A37, A39, A43, A45, A46, A42, MATRIX13:17;

hence A * (i,j) = (Segm (MV,(Seg (dim W)),N)) * (x,y) by A14, A29, A39, A45, MATRIX13:def 1

.= MV * (i,j) by A39, A45, A47, MATRIX13:def 1 ;

:: thesis: verum

end;A43: rng (Sgm N) = N by A12, FINSEQ_1:def 13;

dom (Sgm N) = Seg (dim W) by A12, A13, FINSEQ_3:40;

then consider y being object such that

A44: y in Seg (dim W) and

A45: (Sgm N) . y = j by A41, A43, FUNCT_1:def 3;

reconsider y = y as Element of NAT by A44;

A46: [:(Seg (dim W)),N:] c= Indices A by A12, A33, ZFMISC_1:95;

then A47: [x,y] in Indices (Segm (MV,(Seg (dim W)),N)) by A36, A37, A39, A43, A45, A42, MATRIX13:17;

[x,y] in Indices (Segm (A,(Seg (dim W)),N)) by A37, A39, A43, A45, A46, A42, MATRIX13:17;

hence A * (i,j) = (Segm (MV,(Seg (dim W)),N)) * (x,y) by A14, A29, A39, A45, MATRIX13:def 1

.= MV * (i,j) by A39, A45, A47, MATRIX13:def 1 ;

:: thesis: verum

suppose
not j in N
; :: thesis: MV * (i,j) = A * (i,j)

then A48:
j in (Seg m) \ N
by A40, XBOOLE_0:def 5;

then A49: [i,j] in [:(Seg (dim W)),((Seg m) \ N):] by A35, ZFMISC_1:87;

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

dom (Sgm ((Seg m) \ N)) = Seg (m -' (dim W)) by A13, A9, A16, A11, FINSEQ_3:40, XBOOLE_1:36;

then consider y being object such that

A51: y in Seg (m -' (dim W)) and

A52: (Sgm ((Seg m) \ N)) . y = j by A48, A50, FUNCT_1:def 3;

reconsider y = y as Element of NAT by A51;

A53: [:(Seg (dim W)),((Seg m) \ N):] c= Indices A by A25, A33, ZFMISC_1:95;

then A54: [x,y] in Indices (Segm (A,(Seg (dim W)),((Seg m) \ N))) by A37, A39, A50, A52, A49, MATRIX13:17;

A55: [x,y] in Indices (Segm (MV,(Seg (dim W)),((Seg m) \ N))) by A36, A37, A39, A50, A52, A53, A49, MATRIX13:17;

then A56: [x,y] in Indices ((Segm (M,(Seg (m -' (dim W))),N)) @) by A30, Lm1;

then A57: [y,x] in Indices (Segm (M,(Seg (m -' (dim W))),N)) by MATRIX_0:def 6;

then A58: [y,x] in Indices ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) by A27, Lm1;

thus MV * (i,j) = (- ((Segm (M,(Seg (m -' (dim W))),N)) @)) * (x,y) by A30, A39, A52, A55, MATRIX13:def 1

.= - (((Segm (M,(Seg (m -' (dim W))),N)) @) * (x,y)) by A56, MATRIX_3:def 2

.= - ((- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)) * (y,x)) by A27, A57, MATRIX_0:def 6

.= - (- (((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) * (y,x))) by A58, MATRIX_3:def 2

.= ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) * (y,x) by RLVECT_1:17

.= (Segm (A,(Seg (dim W)),((Seg m) \ N))) * (x,y) by A54, MATRIX_0:def 6

.= A * (i,j) by A39, A52, A54, MATRIX13:def 1 ; :: thesis: verum

end;then A49: [i,j] in [:(Seg (dim W)),((Seg m) \ N):] by A35, ZFMISC_1:87;

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

dom (Sgm ((Seg m) \ N)) = Seg (m -' (dim W)) by A13, A9, A16, A11, FINSEQ_3:40, XBOOLE_1:36;

then consider y being object such that

A51: y in Seg (m -' (dim W)) and

A52: (Sgm ((Seg m) \ N)) . y = j by A48, A50, FUNCT_1:def 3;

reconsider y = y as Element of NAT by A51;

A53: [:(Seg (dim W)),((Seg m) \ N):] c= Indices A by A25, A33, ZFMISC_1:95;

then A54: [x,y] in Indices (Segm (A,(Seg (dim W)),((Seg m) \ N))) by A37, A39, A50, A52, A49, MATRIX13:17;

A55: [x,y] in Indices (Segm (MV,(Seg (dim W)),((Seg m) \ N))) by A36, A37, A39, A50, A52, A53, A49, MATRIX13:17;

then A56: [x,y] in Indices ((Segm (M,(Seg (m -' (dim W))),N)) @) by A30, Lm1;

then A57: [y,x] in Indices (Segm (M,(Seg (m -' (dim W))),N)) by MATRIX_0:def 6;

then A58: [y,x] in Indices ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) by A27, Lm1;

thus MV * (i,j) = (- ((Segm (M,(Seg (m -' (dim W))),N)) @)) * (x,y) by A30, A39, A52, A55, MATRIX13:def 1

.= - (((Segm (M,(Seg (m -' (dim W))),N)) @) * (x,y)) by A56, MATRIX_3:def 2

.= - ((- ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @)) * (y,x)) by A27, A57, MATRIX_0:def 6

.= - (- (((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) * (y,x))) by A58, MATRIX_3:def 2

.= ((Segm (A,(Seg (dim W)),((Seg m) \ N))) @) * (y,x) by RLVECT_1:17

.= (Segm (A,(Seg (dim W)),((Seg m) \ N))) * (x,y) by A54, MATRIX_0:def 6

.= A * (i,j) by A39, A52, A54, MATRIX13:def 1 ; :: thesis: verum

take M ; :: thesis: ex N being finite without_zero Subset of NAT st

( card N = m -' (dim W) & N c= Seg m & Segm (M,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of M )

take (Seg m) \ N ; :: thesis: ( card ((Seg m) \ N) = m -' (dim W) & (Seg m) \ N c= Seg m & Segm (M,(Seg (m -' (dim W))),((Seg m) \ N)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of M )

MV = A by A32, MATRIX_0:27;

then Lin lA = ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) by A15, VECTSP_7:def 3;

hence ( card ((Seg m) \ N) = m -' (dim W) & (Seg m) \ N c= Seg m & Segm (M,(Seg (m -' (dim W))),((Seg m) \ N)) = 1. (K,(m -' (dim W))) & W = Space_of_Solutions_of M ) by A1, A13, A16, A11, A28, A31, VECTSP_9:17, XBOOLE_1:36, XREAL_1:233; :: thesis: verum