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 ;
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 ; :: 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 ;
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 ;
Segm n c= Segm (card (Seg m)) by ;
then A13: n <= m by ;
then A14: m -' n = m - n by XREAL_1:233;
then width (Segm (A,(Seg n),((Seg m) \ N))) = m -' n by ;
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 ;
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 ;
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 () \ ([:(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 ;
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 ; :: 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 ;
A20: width M = l by ;
then A21: width (A * M) = l by ;
len A = n by ;
then len (A * M) = n by ;
then reconsider AM = A * M as Matrix of n,l,K by ;
A22: Indices A = [:(Seg n),(Seg m):] by ;
then A23: [:(Seg n),N:] c= Indices A by ;
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 ;
then A27: I in Seg n by ;
A28: J in Seg l by ;
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 ;
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
.= (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 ;
A34: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by ;
A35: dom (Sgm ((Seg m) \ N)) = Seg (m -' n) by ;
then A36: (Sgm ((Seg m) \ N)) . jj in (Seg m) \ N by ;
then A37: (Line (A,I)) . ((Sgm ((Seg m) \ N)) . jj) = A * (I,((Sgm ((Seg m) \ N)) . jj)) by ;
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
.= (1. (K,(m -' n))) * (jj,jj) by
.= 1_ K by ;
A41: len (Line (A,I)) = m by ;
A42: I = () . I by
.= (Sgm (Seg n)) . I by FINSEQ_3:48 ;
len (Line (V,jj)) = m by ;
then len (mlt ((Line (A,I)),(Line (V,jj)))) = m by ;
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
.= (A * (I,((Sgm ((Seg m) \ N)) . jj))) * (1_ K) by
.= 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 ;
A46: rng (Sgm N) = N by ;
A47: rng (Sgm (Seg n)) = Seg n by FINSEQ_1:def 13;
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 ;
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 ;
reconsider x = x as Element of NAT by A52;
A54: (Line (V,jj)) . ((Sgm N) . x) = V * (jj,((Sgm N) . x)) by ;
[((Sgm (Seg n)) . I),((Sgm N) . x)] in Indices A by ;
then A55: [I,x] in Indices (Segm (A,(Seg n),N)) by ;
(Line (A,I)) . ((Sgm N) . x) = A * (I,((Sgm N) . x)) by
.= (Segm (A,(Seg n),N)) * (I,x) by
.= 0. K by ;
hence (mlt ((Line (A,I)),(Line (V,jj)))) . kk = (0. K) * (V * (jj,((Sgm N) . x))) by
.= 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 ;
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 ;
A59: [jj,x] in Indices (1. (K,(m -' n))) by ;
(Line (V,jj)) . ((Sgm ((Seg m) \ N)) . x) = V * (jj,((Sgm ((Seg m) \ N)) . x)) by
.= (1. (K,(m -' n))) * (jj,x) by
.= 0. K by ;
hence (mlt ((Line (A,I)),(Line (V,jj)))) . kk = (A * (I,((Sgm ((Seg m) \ N)) . x))) * (0. K) by
.= 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 ;
then A60: (Sgm N) . I in N by ;
then A61: (Sgm ((Seg m) \ N)) . jj <> (Sgm N) . I by ;
[((Sgm (Seg n)) . I),((Sgm N) . I)] in Indices A by ;
then A62: [I,I] in Indices (Segm (A,(Seg n),N)) by ;
Indices V = [:(Seg (m -' n)),(Seg m):] by ;
then [((Sgm (Seg (m -' n))) . jj),((Sgm N) . I)] in Indices V by ;
then A63: [jj,I] in Indices (Segm (V,(Seg (m -' n)),N)) by ;
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 ;
A66: (Line (V,jj)) . ((Sgm N) . I) = V * (jj,((Sgm N) . I)) by
.= (Segm (V,(Seg (m -' n)),N)) * (jj,I) by
.= - (((Segm (A,(Seg n),((Seg m) \ N))) @) * (jj,I)) by
.= - ((Segm (A,(Seg n),((Seg m) \ N))) * (I,jj)) by
.= - (A * (I,((Sgm ((Seg m) \ N)) . jj))) by ;
A67: (Line (A,I)) . ((Sgm N) . I) = A * (I,((Sgm N) . I)) by
.= (Segm (A,(Seg n),N)) * (I,I) by
.= 1_ K by ;
(mlt ((Line (A,I)),(Line (V,jj)))) /. ((Sgm N) . I) = (mlt ((Line (A,I)),(Line (V,jj)))) . ((Sgm N) . I) by
.= (1_ K) * (- (A * (I,((Sgm ((Seg m) \ N)) . jj)))) by
.= - (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
.= AM * (i,j) by ;
:: 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
.= Sum ((0. K) * (Line (A,I))) by
.= (0. K) * (Sum (Line (A,I))) by FVSUM_1:73
.= 0. K
.= (0. (K,n,l)) * (i,j) by ;
:: 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