let n, m 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:78;
then A7: card ((Seg m) \ N) = m - n by A1, A2, CARD_2:63;
set ZERO = 0. K,(m -' n),m;
A8: (Seg m) \ N c= Seg m by XBOOLE_1:36;

A9: now

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 FINSEQ_1:4, ZFMISC_1:113;
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 XBOOLE_1:2; :: 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_1:24;
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:119; :: thesis: verum

end;

end;

end;

set SA = Segm A,(Seg n),((Seg m) \ N);
card (Seg n) = n by FINSEQ_1:78;
then A10: len (Segm A,(Seg n),((Seg m) \ N)) = n by A4, MATRIX_1:24;
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_1:24;
n c= card (Seg m) by A1, A2, CARD_1:27;
then A13: n <= m by A6, NAT_1:40;
then A14: m -' n = m - n by XREAL_1:235;
then width (Segm A,(Seg n),((Seg m) \ N)) = m -' n by A4, A7, MATRIX_1:24;
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_1:def 7, MATRIX_2:12;
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_2:7;
then reconsider SAT = - ((Segm A,(Seg n),((Seg m) \ N)) @ ) as Matrix of m -' n,n,K by MATRIX_1: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:122
.= [:(Seg (m -' n)),{} :] by A15, XBOOLE_0:def 7
.= {} by ZFMISC_1:113 ;
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:78;
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_1:24, MATRIX_1:def 3;
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_1:24;
A20: width M = l by A4, A13, MATRIX_1:24;
then A21: width (A * M) = l by A12, A19, MATRIX_3:def 4;
len A = n by A4, MATRIX_1:24;
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_2:7;
A22: Indices A = [:(Seg n),(Seg m):] by A4, MATRIX_1:24;
then A23: [:(Seg n),N:] c= Indices A by A2, ZFMISC_1:119;

now

A24: Indices AM = Indices (0. K,n,l) by MATRIX_1:27;
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 13;
A26: Indices AM = [:(Seg n),(Seg l):] by A4, MATRIX_1:24;
then A27: I in Seg n by A25, ZFMISC_1:106;
A28: J in Seg l by A25, A26, ZFMISC_1:106;

now

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:57
.= (Sgm (Seg (m -' n))) . jj by FINSEQ_3:54 ;
A32: Indices (1. K,(m -' n)) = [:(Seg (m -' n)),(Seg (m -' n)):] by MATRIX_1:25;
then A33: [jj,jj] in Indices (1. K,(m -' n)) by A29, ZFMISC_1:106;
A34: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by A8, FINSEQ_1:def 13;
A35: dom (Sgm ((Seg m) \ N)) = Seg (m -' n) by A14, A7, FINSEQ_3:45, XBOOLE_1:36;
then A36: (Sgm ((Seg m) \ N)) . jj in (Seg m) \ N by A29, A34, FUNCT_1:def 5;
then A37: (Line A,I) . ((Sgm ((Seg m) \ N)) . jj) = A * I,((Sgm ((Seg m) \ N)) . jj) by A12, A8, MATRIX_1:def 8;
A38: m -' n <> 0 by A29;
then A39: width V = m by MATRIX_1:24;
then A40: (Line V,jj) . ((Sgm ((Seg m) \ N)) . jj) = V * jj,((Sgm ((Seg m) \ N)) . jj) by A8, A36, MATRIX_1:def 8
.= (1. K,(m -' n)) * jj,jj by A17, A31, A33, MATRIX13:def 1
.= 1_ K by A33, MATRIX_1:def 12 ;
A41: len (Line A,I) = m by A12, MATRIX_1:def 8;
A42: I = (idseq n) . I by A27, FINSEQ_2:57
.= (Sgm (Seg n)) . I by FINSEQ_3:54 ;
len (Line V,jj) = m by A39, MATRIX_1:def 8;
then len (mlt (Line A,I),(Line V,jj)) = m by A41, MATRIX_3:8;
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 8
.= (A * I,((Sgm ((Seg m) \ N)) . jj)) * (1_ K) by A12, A8, A39, A36, A37, A40, FVSUM_1:74
.= A * I,((Sgm ((Seg m) \ N)) . jj) by VECTSP_1:def 16 ;
A45: ( Indices V = Indices (0. K,(m -' n),m) & rng (Sgm (Seg (m -' n))) = Seg (m -' n) ) by FINSEQ_1:def 13, MATRIX_1:27;
A46: rng (Sgm N) = N by A2, FINSEQ_1:def 13;
A47: rng (Sgm (Seg n)) = Seg n by FINSEQ_1:def 13;

A48: now

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

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 set such that
A52: x in dom (Sgm N) and
A53: (Sgm N) . x = kk by A46, FUNCT_1:def 5;
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_1:def 8;
[((Sgm (Seg n)) . I),((Sgm N) . x)] in Indices A by A22, A27, A42, A49, A53, ZFMISC_1:106;
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_1:def 8
.= (Segm A,(Seg n),N) * I,x by A42, A55, MATRIX13:def 1
.= 0. K by A3, A51, A53, A55, MATRIX_1:def 12 ;
hence (mlt (Line A,I),(Line V,jj)) . kk = (0. K) * (V * jj,((Sgm N) . x)) by A12, A39, A49, A53, A54, FVSUM_1:74
.= 0. K by VECTSP_1:39 ;
:: thesis: verum

end;

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

then consider x being set such that
A56: x in dom (Sgm ((Seg m) \ N)) and
A57: (Sgm ((Seg m) \ N)) . x = kk by A34, FUNCT_1:def 5;
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_1:def 8;
A59: [jj,x] in Indices (1. K,(m -' n)) by A29, A35, A32, A56, ZFMISC_1:106;
(Line V,jj) . ((Sgm ((Seg m) \ N)) . x) = V * jj,((Sgm ((Seg m) \ N)) . x) by A39, A49, A57, MATRIX_1:def 8
.= (1. K,(m -' n)) * jj,x by A17, A31, A59, MATRIX13:def 1
.= 0. K by A50, A57, A59, MATRIX_1:def 12 ;
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:74
.= 0. K by VECTSP_1:39 ;
:: 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, A2, FINSEQ_3:45;
then A60: (Sgm N) . I in N by A27, A46, FUNCT_1:def 5;
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:106;
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_1:24;
then [((Sgm (Seg (m -' n))) . jj),((Sgm N) . I)] in Indices V by A2, A29, A60, A31, ZFMISC_1:106;
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_1:def 7;
A66: (Line V,jj) . ((Sgm N) . I) = V * jj,((Sgm N) . I) by A2, A39, A60, MATRIX_1:def 8
.= (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_1:def 7
.= - (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_1:def 8
.= (Segm A,(Seg n),N) * I,I by A42, A62, MATRIX13:def 1
.= 1_ K by A3, A62, MATRIX_1:def 12 ;
(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 8
.= (1_ K) * (- (A * I,((Sgm ((Seg m) \ N)) . jj))) by A2, A12, A39, A60, A67, A66, FVSUM_1:74
.= - (A * I,((Sgm ((Seg m) \ N)) . jj)) by VECTSP_1:def 16 ;
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:63 ;
hence (0. K,n,l) * i,j = (Line A,I) "*" (Line V,jj) by A25, A24, MATRIX_3:3
.= 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:80
.= (0. K) * (Sum (Line A,I)) by FVSUM_1:92
.= 0. K by VECTSP_1:36
.= (0. K,n,l) * i,j by A25, A24, MATRIX_3:3 ;
:: 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_1:28;
hence M in Solutions_of A,(0. K,n,l) by A12, A19, A20, A21; :: thesis: verum