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 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))) @) & ( 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 (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l))) ) )
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 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))) @) & ( 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 (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l))) ) )
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 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))) @) & ( 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 (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l))) ) )
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 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))) @) & ( 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 (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l))) ) ) )
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 ; :: 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))) @) & ( 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 (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l))) ) )
set SN = (Seg m) \ N;
A5: ( m -' n = 0 or m -' n > 0 ) ;
A6: card (Seg m) = m by FINSEQ_1:57;
then A7: card ((Seg m) \ N) = m - n by A1, A2, CARD_2:44;
set ZERO = 0. (K,(m -' n),m);
A8: (Seg m) \ N c= Seg m by XBOOLE_1:36;

A9: now :: thesis: ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) )

per cases ( m -' n = 0 or m -' n > 0 ) ;

suppose m -' n = 0 ; :: thesis: ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) )

then Seg (m -' n) = {} ;
then ( [:(Seg (m -' n)),N:] = {} & [:(Seg (m -' n)),((Seg m) \ N):] = {} ) by ZFMISC_1:90;
hence ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) ) ; :: thesis: verum

end;

suppose m -' n > 0 ; :: thesis: ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) )

then Indices (0. (K,(m -' n),m)) = [:(Seg (m -' n)),(Seg m):] by MATRIX_0:23;
hence ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) ) by A2, A8, ZFMISC_1:96; :: thesis: verum

end;

end;

end;

set SA = Segm (A,(Seg n),((Seg m) \ N));
card (Seg n) = n by FINSEQ_1:57;
then A10: len (Segm (A,(Seg n),((Seg m) \ N))) = n by A4, MATRIX_0:23;
A11: ( len ((Segm (A,(Seg n),((Seg m) \ N))) @) = len (- ((Segm (A,(Seg n),((Seg m) \ N))) @)) & width ((Segm (A,(Seg n),((Seg m) \ N))) @) = width (- ((Segm (A,(Seg n),((Seg m) \ N))) @)) ) by MATRIX_3:def 2;
A12: width A = m by A4, MATRIX_0:23;
Segm n c= Segm (card (Seg m)) by A1, A2, CARD_1:11;
then A13: n <= m by A6, NAT_1:39;
then A14: m -' n = m - n by XREAL_1:233;
then width (Segm (A,(Seg n),((Seg m) \ N))) = m -' n by A4, A7, MATRIX_0:23;
then ( ( len ((Segm (A,(Seg n),((Seg m) \ N))) @) = 0 & m -' n = 0 ) or ( len ((Segm (A,(Seg n),((Seg m) \ N))) @) = m -' n & width ((Segm (A,(Seg n),((Seg m) \ N))) @) = n ) ) by A10, A5, MATRIX_0:54, MATRIX_0:def 6;
then ( ( - ((Segm (A,(Seg n),((Seg m) \ N))) @) = {} & m -' n = 0 ) or - ((Segm (A,(Seg n),((Seg m) \ N))) @) is Matrix of m -' n,n,K ) by A11, MATRIX_0:51;
then reconsider SAT = - ((Segm (A,(Seg n),((Seg m) \ N))) @) as Matrix of m -' n,n,K by MATRIX_0:13;
set ONE = 1. (K,(m -' n));
A15: N misses (Seg m) \ N by XBOOLE_1:79;
[:(Seg (m -' n)),N:] /\ [:(Seg (m -' n)),((Seg m) \ N):] = [:(Seg (m -' n)),(N /\ ((Seg m) \ N)):] by ZFMISC_1:99
.= [:(Seg (m -' n)),{}:] by A15
.= {} by ZFMISC_1:90 ;
then ( card (Seg (m -' n)) = m -' n & ( for i, j, bi, bj, ci, cj being Nat st [i,j] in [:(Seg (m -' n)),N:] /\ [:(Seg (m -' n)),((Seg m) \ N):] & bi = ((Sgm (Seg (m -' n))) ") . i & bj = ((Sgm N) ") . j & ci = ((Sgm (Seg (m -' n))) ") . i & cj = ((Sgm ((Seg m) \ N)) ") . j holds
SAT * (bi,bj) = (1. (K,(m -' n))) * (ci,cj) ) ) by FINSEQ_1:57;
then consider V being Matrix of len (0. (K,(m -' n),m)), width (0. (K,(m -' n),m)),K such that
A16: Segm (V,(Seg (m -' n)),N) = SAT and
A17: Segm (V,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) and
for i, j being Nat st [i,j] in (Indices V) \ ([:(Seg (m -' n)),N:] \/ [:(Seg (m -' n)),((Seg m) \ N):]) holds
V * (i,j) = (0. (K,(m -' n),m)) * (i,j) by A1, A9, A14, A7, Th9;
( m -' n = 0 or m -' n > 0 ) ;
then ( ( len (0. (K,(m -' n),m)) = 0 & m -' n = 0 & len V = len (0. (K,(m -' n),m)) ) or ( len (0. (K,(m -' n),m)) = m -' n & width (0. (K,(m -' n),m)) = m ) ) by MATRIX_0:23, MATRIX_0:def 2;
then ( ( V = {} & m -' n = 0 ) or V is Matrix of m -' n,m,K ) ;
then reconsider V = V as Matrix of m -' n,m,K ;
take V ; :: thesis: ( Segm (V,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (V,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( 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 (V,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l))) ) )
thus ( Segm (V,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (V,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) ) by A16, A17; :: thesis: 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 (V,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l)))
let l be Nat; :: thesis: 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 (V,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l)))
let M be Matrix of m,l,K; :: thesis: ( ( 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 (V,j) ) or Col (M,i) = m |-> (0. K) ) ) implies M in Solutions_of (A,(0. (K,n,l))) )
assume A18: 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 (V,j) ) or Col (M,i) = m |-> (0. K) ) ; :: thesis: M in Solutions_of (A,(0. (K,n,l)))
set Z = 0. (K,n,l);
A19: len M = m by A4, A13, MATRIX_0:23;
A20: width M = l by A4, A13, MATRIX_0:23;
then A21: width (A * M) = l by A12, A19, MATRIX_3:def 4;
len A = n by A4, MATRIX_0:23;
then len (A * M) = n by A12, A19, MATRIX_3:def 4;
then reconsider AM = A * M as Matrix of n,l,K by A21, MATRIX_0:51;
A22: Indices A = [:(Seg n),(Seg m):] by A4, MATRIX_0:23;
then A23: [:(Seg n),N:] c= Indices A by A2, ZFMISC_1:96;

now :: thesis: for i, j being Nat st [i,j] in Indices AM holds
AM * (i,j) = (0. (K,n,l)) * (i,j)

A24: Indices AM = Indices (0. (K,n,l)) by MATRIX_0:26;
let i, j be Nat; :: thesis: ( [i,j] in Indices AM implies AM * (i,j) = (0. (K,n,l)) * (i,j) )
assume A25: [i,j] in Indices AM ; :: thesis: AM * (i,j) = (0. (K,n,l)) * (i,j)
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;
A26: Indices AM = [:(Seg n),(Seg l):] by A4, MATRIX_0:23;
then A27: I in Seg n by A25, ZFMISC_1:87;
A28: J in Seg l by A25, A26, ZFMISC_1:87;

now :: thesis: (0. (K,n,l)) * (i,j) = AM * (i,j)

per cases ( ex jj being Nat st
( jj in Seg (m -' n) & Col (M,J) = Line (V,jj) ) or Col (M,J) = m |-> (0. K) ) by A18, A28;

suppose ex jj being Nat st
( jj in Seg (m -' n) & Col (M,J) = Line (V,jj) ) ; :: thesis: (0. (K,n,l)) * (i,j) = AM * (i,j)

then consider jj being Nat such that
A29: jj in Seg (m -' n) and
A30: Col (M,J) = Line (V,jj) ;
A31: jj = (idseq (m -' n)) . jj by A29, FINSEQ_2:49
.= (Sgm (Seg (m -' n))) . jj by FINSEQ_3:48 ;
A32: Indices (1. (K,(m -' n))) = [:(Seg (m -' n)),(Seg (m -' n)):] by MATRIX_0:24;
then A33: [jj,jj] in Indices (1. (K,(m -' n))) by A29, ZFMISC_1:87;
A34: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by FINSEQ_1:def 14;
A35: dom (Sgm ((Seg m) \ N)) = Seg (m -' n) by A14, A7, FINSEQ_3:40;
then A36: (Sgm ((Seg m) \ N)) . jj in (Seg m) \ N by A29, A34, FUNCT_1:def 3;
then A37: (Line (A,I)) . ((Sgm ((Seg m) \ N)) . jj) = A * (I,((Sgm ((Seg m) \ N)) . jj)) by A12, A8, MATRIX_0:def 7;
A38: m -' n <> 0 by A29;
then A39: width V = m by MATRIX_0:23;
then A40: (Line (V,jj)) . ((Sgm ((Seg m) \ N)) . jj) = V * (jj,((Sgm ((Seg m) \ N)) . jj)) by A8, A36, MATRIX_0:def 7
.= (1. (K,(m -' n))) * (jj,jj) by A17, A31, A33, MATRIX13:def 1
.= 1_ K by A33, MATRIX_1:def 3 ;
A41: len (Line (A,I)) = m by A12, MATRIX_0:def 7;
A42: I = (idseq n) . I by A27, FINSEQ_2:49
.= (Sgm (Seg n)) . I by FINSEQ_3:48 ;
len (Line (V,jj)) = m by A39, MATRIX_0:def 7;
then len (mlt ((Line (A,I)),(Line (V,jj)))) = m by A41, MATRIX_3:6;
then A43: dom (mlt ((Line (A,I)),(Line (V,jj)))) = Seg m by FINSEQ_1:def 3;
then A44: (mlt ((Line (A,I)),(Line (V,jj)))) /. ((Sgm ((Seg m) \ N)) . jj) = (mlt ((Line (A,I)),(Line (V,jj)))) . ((Sgm ((Seg m) \ N)) . jj) by A8, A36, PARTFUN1:def 6
.= (A * (I,((Sgm ((Seg m) \ N)) . jj))) * (1_ K) by A12, A8, A39, A36, A37, A40, FVSUM_1:61
.= A * (I,((Sgm ((Seg m) \ N)) . jj)) ;
A45: ( Indices V = Indices (0. (K,(m -' n),m)) & rng (Sgm (Seg (m -' n))) = Seg (m -' n) ) by FINSEQ_1:def 14, MATRIX_0:26;
A46: rng (Sgm N) = N by FINSEQ_1:def 14;
A47: rng (Sgm (Seg n)) = Seg n by FINSEQ_1:def 14;

A48: now :: thesis: for kk being Nat st kk in Seg m & kk <> (Sgm ((Seg m) \ N)) . jj & kk <> (Sgm N) . I holds
(mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

let kk be Nat; :: thesis: ( kk in Seg m & kk <> (Sgm ((Seg m) \ N)) . jj & kk <> (Sgm N) . I implies (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K )
assume that
A49: kk in Seg m and
A50: kk <> (Sgm ((Seg m) \ N)) . jj and
A51: kk <> (Sgm N) . I ; :: thesis: (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

now :: thesis: (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

per cases ( kk in N or kk in (Seg m) \ N ) by A49, XBOOLE_0:def 5;

suppose kk in N ; :: thesis: (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

then consider x being object such that
A52: x in dom (Sgm N) and
A53: (Sgm N) . x = kk by A46, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A52;
A54: (Line (V,jj)) . ((Sgm N) . x) = V * (jj,((Sgm N) . x)) by A39, A49, A53, MATRIX_0:def 7;
[((Sgm (Seg n)) . I),((Sgm N) . x)] in Indices A by A22, A27, A42, A49, A53, ZFMISC_1:87;
then A55: [I,x] in Indices (Segm (A,(Seg n),N)) by A23, A46, A47, MATRIX13:17;
(Line (A,I)) . ((Sgm N) . x) = A * (I,((Sgm N) . x)) by A12, A49, A53, MATRIX_0:def 7
.= (Segm (A,(Seg n),N)) * (I,x) by A42, A55, MATRIX13:def 1
.= 0. K by A3, A51, A53, A55, MATRIX_1:def 3 ;
hence (mlt ((Line (A,I)),(Line (V,jj)))) . kk = (0. K) * (V * (jj,((Sgm N) . x))) by A12, A39, A49, A53, A54, FVSUM_1:61
.= 0. K ;
:: thesis: verum

end;

suppose kk in (Seg m) \ N ; :: thesis: (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

then consider x being object such that
A56: x in dom (Sgm ((Seg m) \ N)) and
A57: (Sgm ((Seg m) \ N)) . x = kk by A34, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A56;
A58: (Line (A,I)) . ((Sgm ((Seg m) \ N)) . x) = A * (I,((Sgm ((Seg m) \ N)) . x)) by A12, A49, A57, MATRIX_0:def 7;
A59: [jj,x] in Indices (1. (K,(m -' n))) by A29, A35, A32, A56, ZFMISC_1:87;
(Line (V,jj)) . ((Sgm ((Seg m) \ N)) . x) = V * (jj,((Sgm ((Seg m) \ N)) . x)) by A39, A49, A57, MATRIX_0:def 7
.= (1. (K,(m -' n))) * (jj,x) by A17, A31, A59, MATRIX13:def 1
.= 0. K by A50, A57, A59, MATRIX_1:def 3 ;
hence (mlt ((Line (A,I)),(Line (V,jj)))) . kk = (A * (I,((Sgm ((Seg m) \ N)) . x))) * (0. K) by A12, A39, A49, A57, A58, FVSUM_1:61
.= 0. K ;
:: thesis: verum

end;

end;

end;

hence (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K ; :: thesis: verum

end;

dom (Sgm N) = Seg n by A1, FINSEQ_3:40;
then A60: (Sgm N) . I in N by A27, A46, FUNCT_1:def 3;
then A61: (Sgm ((Seg m) \ N)) . jj <> (Sgm N) . I by A15, A36, XBOOLE_0:3;
[((Sgm (Seg n)) . I),((Sgm N) . I)] in Indices A by A2, A22, A27, A60, A42, ZFMISC_1:87;
then A62: [I,I] in Indices (Segm (A,(Seg n),N)) by A23, A46, A47, MATRIX13:17;
Indices V = [:(Seg (m -' n)),(Seg m):] by A38, MATRIX_0:23;
then [((Sgm (Seg (m -' n))) . jj),((Sgm N) . I)] in Indices V by A2, A29, A60, A31, ZFMISC_1:87;
then A63: [jj,I] in Indices (Segm (V,(Seg (m -' n)),N)) by A9, A46, A45, MATRIX13:17;
A64: Indices SAT = Indices ((Segm (A,(Seg n),((Seg m) \ N))) @) by Lm1;
then A65: [I,jj] in Indices (Segm (A,(Seg n),((Seg m) \ N))) by A16, A63, MATRIX_0:def 6;
A66: (Line (V,jj)) . ((Sgm N) . I) = V * (jj,((Sgm N) . I)) by A2, A39, A60, MATRIX_0:def 7
.= (Segm (V,(Seg (m -' n)),N)) * (jj,I) by A31, A63, MATRIX13:def 1
.= - (((Segm (A,(Seg n),((Seg m) \ N))) @) * (jj,I)) by A16, A63, A64, MATRIX_3:def 2
.= - ((Segm (A,(Seg n),((Seg m) \ N))) * (I,jj)) by A65, MATRIX_0:def 6
.= - (A * (I,((Sgm ((Seg m) \ N)) . jj))) by A42, A65, MATRIX13:def 1 ;
A67: (Line (A,I)) . ((Sgm N) . I) = A * (I,((Sgm N) . I)) by A2, A12, A60, MATRIX_0:def 7
.= (Segm (A,(Seg n),N)) * (I,I) by A42, A62, MATRIX13:def 1
.= 1_ K by A3, A62, MATRIX_1:def 3 ;
(mlt ((Line (A,I)),(Line (V,jj)))) /. ((Sgm N) . I) = (mlt ((Line (A,I)),(Line (V,jj)))) . ((Sgm N) . I) by A2, A43, A60, PARTFUN1:def 6
.= (1_ K) * (- (A * (I,((Sgm ((Seg m) \ N)) . jj)))) by A2, A12, A39, A60, A67, A66, FVSUM_1:61
.= - (A * (I,((Sgm ((Seg m) \ N)) . jj))) ;
then Sum (mlt ((Line (A,I)),(Line (V,jj)))) = (A * (I,((Sgm ((Seg m) \ N)) . jj))) + (- (A * (I,((Sgm ((Seg m) \ N)) . jj)))) by A2, A8, A43, A60, A36, A44, A61, A48, Th7
.= 0. K by VECTSP_1:16 ;
hence (0. (K,n,l)) * (i,j) = (Line (A,I)) "*" (Line (V,jj)) by A25, A24, MATRIX_3:1
.= AM * (i,j) by A12, A19, A25, A30, MATRIX_3:def 4 ;
:: thesis: verum

end;

suppose Col (M,J) = m |-> (0. K) ; :: thesis: AM * (i,j) = (0. (K,n,l)) * (i,j)

hence AM * (i,j) = (Line (A,I)) "*" (m |-> (0. K)) by A12, A19, A25, MATRIX_3:def 4
.= Sum ((0. K) * (Line (A,I))) by A12, FVSUM_1:66
.= (0. K) * (Sum (Line (A,I))) by FVSUM_1:73
.= 0. K
.= (0. (K,n,l)) * (i,j) by A25, A24, MATRIX_3:1 ;
:: thesis: verum

end;

end;

end;

hence AM * (i,j) = (0. (K,n,l)) * (i,j) ; :: thesis: verum

end;

then AM = 0. (K,n,l) by MATRIX_0:27;
hence M in Solutions_of (A,(0. (K,n,l))) by A12, A19, A20, A21; :: thesis: verum