let n, m be Nat; :: thesis:
let K be Field; :: thesis:
let A be Matrix of n,m,K; :: thesis:
let N be finite without_zero Subset of NAT ; :: thesis:
assume that
A1: ( card N = n & N c= Seg m ) and
A2: Segm A,(Seg n),N = 1. K,n and
A3: n > 0 ; :: thesis:
A4: ( len A = n & width A = m & Indices A = [:(Seg n),(Seg m):] ) by A3, MATRIX_1:24;
set SN = (Seg m) \ N;
A5: (Seg m) \ N c= Seg m by XBOOLE_1:36;
then A6: ( [:(Seg n),N:] c= Indices A & [:(Seg n),((Seg m) \ N):] c= Indices A ) by A1, A4, ZFMISC_1:119;
set ZERO = 0. K,(m -' n),m;

A7: now

per cases ;

suppose m -' n = 0 ; :: thesis:

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:

end;

suppose m -' n > 0 ; :: thesis:

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 A1, A5, ZFMISC_1:119; :: thesis:

end;

A8: ( card (Seg m) = m & card (Seg n) = n & card (Seg (m -' n)) = m -' n ) by FINSEQ_1:78;
n c= card (Seg m) by A1, CARD_1:27;
then A9: n <= m by A8, NAT_1:40;
then A10: ( m -' n = m - n & card ((Seg m) \ N) = m - n ) by A1, A8, CARD_2:63, XREAL_1:235;
set SA = Segm A,(Seg n),((Seg m) \ N);
set ONE = 1. K,(m -' n);
A11: ( len (Segm A,(Seg n),((Seg m) \ N)) = n & width (Segm A,(Seg n),((Seg m) \ N)) = m -' n ) by A3, A8, A10, MATRIX_1:24;
( m -' n = 0 or m -' n > 0 ) ;
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 ) ) & 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 A11, MATRIX_1:def 7, MATRIX_2:12, MATRIX_3:def 2;
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 MATRIX_2:7;
then reconsider SAT = - ((Segm A,(Seg n),((Seg m) \ N)) @ ) as Matrix of m -' n,n,K by MATRIX_1:13;
A12: 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 A12, XBOOLE_0:def 7
.= {} by ZFMISC_1:113 ;
then 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 ;
then consider V being Matrix of len (0. K,(m -' n),m), width (0. K,(m -' n),m),K such that
A13: ( Segm V,(Seg (m -' n)),N = SAT & 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, A7, A8, A10, 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:
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 A13; :: thesis:
let l be Nat; :: thesis:
let M be Matrix of m,l,K; :: thesis:
assume A14: 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:
set Z = 0. K,n,l;
A15: ( len M = m & width M = l ) by A3, A9, MATRIX_1:24;
then A16: ( len (A * M) = n & width (A * M) = l & width (0. K,n,l) = l ) by A3, A4, MATRIX_1:24, MATRIX_3:def 4;
then reconsider AM = A * M as Matrix of n,l,K by MATRIX_2:7;

now

let i, j be Nat; :: thesis:
assume A17: [i,j] in Indices AM ; :: thesis:
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 13;
A18: ( Indices AM = [:(Seg n),(Seg l):] & Indices AM = Indices (0. K,n,l) ) by A3, MATRIX_1:24, MATRIX_1:27;
then A19: ( I in Seg n & J in Seg l ) by A17, ZFMISC_1:106;

now

per cases by A19, A14;

suppose ex jj being Nat st
( jj in Seg (m -' n) & Col M,J = Line V,jj ) ; :: thesis:

then consider jj being Nat such that
A20: jj in Seg (m -' n) and
A21: Col M,J = Line V,jj ;
m -' n <> 0 by A20;
then m -' n > 0 ;
then A22: ( len V = m -' n & width V = m & Indices V = [:(Seg (m -' n)),(Seg m):] & Indices V = Indices (0. K,(m -' n),m) ) by MATRIX_1:24, MATRIX_1:27;
then ( len (Line A,I) = m & len (Line V,jj) = m ) by A4, MATRIX_1:def 8;
then len (mlt (Line A,I),(Line V,jj)) = m by MATRIX_3:8;
then A23: dom (mlt (Line A,I),(Line V,jj)) = Seg m by FINSEQ_1:def 3;
A24: ( dom (Sgm N) = Seg n & rng (Sgm N) = N & dom (Sgm ((Seg m) \ N)) = Seg (m -' n) & rng (Sgm ((Seg m) \ N)) = (Seg m) \ N & rng (Sgm (Seg n)) = Seg n & rng (Sgm (Seg (m -' n))) = Seg (m -' n) & Sgm N is one-to-one & Sgm ((Seg m) \ N) is one-to-one ) by A1, A5, A10, FINSEQ_1:def 13, FINSEQ_3:45, FINSEQ_3:99;
then A25: (Sgm N) . I in N by A19, FUNCT_1:def 5;
A26: I = (idseq n) . I by A19, FINSEQ_2:57
.= (Sgm (Seg n)) . I by FINSEQ_3:54 ;
then [((Sgm (Seg n)) . I),((Sgm N) . I)] in Indices A by A1, A4, A19, A25, ZFMISC_1:106;
then A27: [I,I] in Indices (Segm A,(Seg n),N) by A6, A24, MATRIX13:17;
A28: (Line A,I) . ((Sgm N) . I) = A * I,((Sgm N) . I) by A1, A4, A25, MATRIX_1:def 8
.= (Segm A,(Seg n),N) * I,I by A26, A27, MATRIX13:def 1
.= 1_ K by A2, A27, MATRIX_1:def 12 ;
A29: jj = (idseq (m -' n)) . jj by A20, FINSEQ_2:57
.= (Sgm (Seg (m -' n))) . jj by FINSEQ_3:54 ;
then [((Sgm (Seg (m -' n))) . jj),((Sgm N) . I)] in Indices V by A20, A1, A25, A22, ZFMISC_1:106;
then A30: ( [jj,I] in Indices (Segm V,(Seg (m -' n)),N) & Indices SAT = Indices ((Segm A,(Seg n),((Seg m) \ N)) @ ) ) by A7, A22, A24, Lm1, MATRIX13:17;
then A31: [I,jj] in Indices (Segm A,(Seg n),((Seg m) \ N)) by A13, MATRIX_1:def 7;
A32: (Line V,jj) . ((Sgm N) . I) = V * jj,((Sgm N) . I) by A1, A25, A22, MATRIX_1:def 8
.= (Segm V,(Seg (m -' n)),N) * jj,I by A29, A30, MATRIX13:def 1
.= - (((Segm A,(Seg n),((Seg m) \ N)) @ ) * jj,I) by A13, A30, MATRIX_3:def 2
.= - ((Segm A,(Seg n),((Seg m) \ N)) * I,jj) by A31, MATRIX_1:def 7
.= - (A * I,((Sgm ((Seg m) \ N)) . jj)) by A26, A31, MATRIX13:def 1 ;
A33: (mlt (Line A,I),(Line V,jj)) /. ((Sgm N) . I) = (mlt (Line A,I),(Line V,jj)) . ((Sgm N) . I) by A1, A25, A23, PARTFUN1:def 8
.= (1_ K) * (- (A * I,((Sgm ((Seg m) \ N)) . jj))) by A1, A4, A22, A25, A28, A32, FVSUM_1:74
.= - (A * I,((Sgm ((Seg m) \ N)) . jj)) by VECTSP_1:def 16 ;
A34: (Sgm ((Seg m) \ N)) . jj in (Seg m) \ N by A20, A24, FUNCT_1:def 5;
then A35: (Line A,I) . ((Sgm ((Seg m) \ N)) . jj) = A * I,((Sgm ((Seg m) \ N)) . jj) by A4, A5, MATRIX_1:def 8;
A36: Indices (1. K,(m -' n)) = [:(Seg (m -' n)),(Seg (m -' n)):] by MATRIX_1:25;
then A37: [jj,jj] in Indices (1. K,(m -' n)) by A20, ZFMISC_1:106;
A38: (Line V,jj) . ((Sgm ((Seg m) \ N)) . jj) = V * jj,((Sgm ((Seg m) \ N)) . jj) by A5, A34, A22, MATRIX_1:def 8
.= (1. K,(m -' n)) * jj,jj by A13, A29, A37, MATRIX13:def 1
.= 1_ K by A37, MATRIX_1:def 12 ;
A39: (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 A5, A34, A23, PARTFUN1:def 8
.= (A * I,((Sgm ((Seg m) \ N)) . jj)) * (1_ K) by A4, A5, A22, A35, A38, A34, FVSUM_1:74
.= A * I,((Sgm ((Seg m) \ N)) . jj) by VECTSP_1:def 16 ;
A40: (Sgm ((Seg m) \ N)) . jj <> (Sgm N) . I by A12, A25, A34, XBOOLE_0:3;

now

let kk be Nat; :: thesis:
assume that
A41: kk in Seg m and
A42: ( kk <> (Sgm ((Seg m) \ N)) . jj & kk <> (Sgm N) . I ) ; :: thesis:

now

per cases by A41, XBOOLE_0:def 5;

suppose kk in N ; :: thesis:

then consider x being set such that
A43: ( x in dom (Sgm N) & (Sgm N) . x = kk ) by A24, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A43;
[((Sgm (Seg n)) . I),((Sgm N) . x)] in Indices A by A26, A4, A19, A41, A43, ZFMISC_1:106;
then A44: [I,x] in Indices (Segm A,(Seg n),N) by A6, A24, MATRIX13:17;
A45: (Line A,I) . ((Sgm N) . x) = A * I,((Sgm N) . x) by A4, A41, A43, MATRIX_1:def 8
.= (Segm A,(Seg n),N) * I,x by A26, A44, MATRIX13:def 1
.= 0. K by A2, A44, A43, A42, MATRIX_1:def 12 ;
(Line V,jj) . ((Sgm N) . x) = V * jj,((Sgm N) . x) by A41, A43, A22, MATRIX_1:def 8;
hence (mlt (Line A,I),(Line V,jj)) . kk = (0. K) * (V * jj,((Sgm N) . x)) by A4, A22, A45, A41, A43, FVSUM_1:74
.= 0. K by VECTSP_1:39 ;
:: thesis:

end;

suppose kk in (Seg m) \ N ; :: thesis:

then consider x being set such that
A46: ( x in dom (Sgm ((Seg m) \ N)) & (Sgm ((Seg m) \ N)) . x = kk ) by A24, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A46;
A47: (Line A,I) . ((Sgm ((Seg m) \ N)) . x) = A * I,((Sgm ((Seg m) \ N)) . x) by A4, A41, A46, MATRIX_1:def 8;
A48: [jj,x] in Indices (1. K,(m -' n)) by A20, A46, A24, A36, ZFMISC_1:106;
(Line V,jj) . ((Sgm ((Seg m) \ N)) . x) = V * jj,((Sgm ((Seg m) \ N)) . x) by A22, A41, A46, MATRIX_1:def 8
.= (1. K,(m -' n)) * jj,x by A29, A13, A48, MATRIX13:def 1
.= 0. K by A48, A46, A42, MATRIX_1:def 12 ;
hence (mlt (Line A,I),(Line V,jj)) . kk = (A * I,((Sgm ((Seg m) \ N)) . x)) * (0. K) by A4, A22, A47, A41, A46, FVSUM_1:74
.= 0. K by VECTSP_1:39 ;
:: thesis:

end;

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

end;

then Sum (mlt (Line A,I),(Line V,jj)) = (A * I,((Sgm ((Seg m) \ N)) . jj)) + (- (A * I,((Sgm ((Seg m) \ N)) . jj))) by A33, A39, A23, Th7, A40, A1, A25, A5, A34
.= 0. K by VECTSP_1:63 ;
hence (0. K,n,l) * i,j = (Line A,I) "*" (Line V,jj) by A17, A18, MATRIX_3:3
.= AM * i,j by A4, A15, A17, A21, MATRIX_3:def 4 ;
:: thesis:

end;

suppose Col M,J = m |-> (0. K) ; :: thesis:

hence AM * i,j = (Line A,I) "*" (m |-> (0. K)) by A4, A15, A17, MATRIX_3:def 4
.= Sum ((0. K) * (Line A,I)) by A4, 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 A17, A18, MATRIX_3:3 ;
:: thesis:

end;

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

end;

then AM = 0. K,n,l by MATRIX_1:28;
hence M in Solutions_of A,(0. K,n,l) by A4, A15, A16; :: thesis: