let l, m, n be Nat; :: thesis:
let K be Field; :: thesis:
let A be Matrix of n,m,K; :: thesis:
let B be Matrix of n,l,K; :: thesis:
let N be finite without_zero Subset of NAT; :: thesis:
assume that
A1: card N = n and
A2: N c= Seg m and
A3: n > 0 and
A4: Segm (A,(Seg n),N) = 1. (K,n) ; :: thesis:
A5: width A = m by A3, MATRIX_0:23;
set Z = 0. (K,m,l);
set SN = (Seg m) \ N;
A6: card (Seg m) = m by FINSEQ_1:57;
then A7: ( m -' n = m - n & card ((Seg m) \ N) = m - n ) by A1, A2, CARD_2:44, NAT_1:43, XREAL_1:233;
set ZERO = 0. (K,(m -' n),l);
A8: N misses (Seg m) \ N by XBOOLE_1:79;
[:N,(Seg l):] /\ [:((Seg m) \ N),(Seg l):] = [:(N /\ ((Seg m) \ N)),(Seg l):] by ZFMISC_1:99
.= [:{},(Seg l):] by A8
.= {} by ZFMISC_1:90 ;
then A9: for i, j, bi, bj, ci, cj being Nat st [i,j] in [:N,(Seg l):] /\ [:((Seg m) \ N),(Seg l):] & bi = ((Sgm N) ") . i & bj = ((Sgm (Seg l)) ") . j & ci = ((Sgm ((Seg m) \ N)) ") . i & cj = ((Sgm (Seg l)) ") . j holds
B * (bi,bj) = (0. (K,(m -' n),l)) * (ci,cj) ;
A10: Indices A = [:(Seg n),(Seg m):] by A3, MATRIX_0:23;
A11: n <= card (Seg m) by A1, A2, NAT_1:43;
then A12: ( len (0. (K,m,l)) = m & width (0. (K,m,l)) = l ) by A3, A6, MATRIX_0:23;
A13: Indices (0. (K,m,l)) = [:(Seg m),(Seg l):] by A3, A11, A6, MATRIX_0:23;
then A14: [:N,(Seg l):] c= Indices (0. (K,m,l)) by A2, ZFMISC_1:95;
A15: (Seg m) \ N c= Seg m by XBOOLE_1:36;
then ( card (Seg l) = l & [:((Seg m) \ N),(Seg l):] c= Indices (0. (K,m,l)) ) by A13, FINSEQ_1:57, ZFMISC_1:95;
then consider X being Matrix of m,l,K such that
A16: Segm (X,N,(Seg l)) = B and
A17: Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) and
for i, j being Nat st [i,j] in (Indices X) \ ([:N,(Seg l):] \/ [:((Seg m) \ N),(Seg l):]) holds
X * (i,j) = (0. (K,m,l)) * (i,j) by A1, A7, A12, A14, A9, Th9;
set AX = A * X;
A18: len X = m by A3, A11, A6, MATRIX_0:23;
then A19: dom X = Seg m by FINSEQ_1:def 3;
len A = n by A3, MATRIX_0:23;
then A20: len (A * X) = n by A5, A18, MATRIX_3:def 4;
take X ; :: thesis:
thus ( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) & Segm (X,N,(Seg l)) = B ) by A16, A17; :: thesis:
A21: Indices X = [:(Seg m),(Seg l):] by A3, A11, A6, MATRIX_0:23;
A22: width B = l by A3, MATRIX_0:23;
A23: width X = l by A3, A11, A6, MATRIX_0:23;
then width (A * X) = l by A5, A18, MATRIX_3:def 4;
then reconsider AX = A * X as Matrix of n,l,K by A20, MATRIX_0:51;
A24: Indices B = [:(Seg n),(Seg l):] by A3, MATRIX_0:23;

now :: thesis:

A25: [:N,(Seg l):] c= Indices X by A2, A21, ZFMISC_1:95;
let i, j be Nat; :: thesis:
assume A26: [i,j] in Indices AX ; :: thesis:
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;
A27: Indices AX = Indices B by MATRIX_0:26;
then A28: i in Seg n by A24, A26, ZFMISC_1:87;
( len (Line (A,i)) = m & len (Col (X,j)) = m ) by A5, A18, CARD_1:def 7;
then len (mlt ((Line (A,i)),(Col (X,j)))) = m by MATRIX_3:6;
then A29: dom (mlt ((Line (A,i)),(Col (X,j)))) = Seg m by FINSEQ_1:def 3;
A30: rng (Sgm (Seg l)) = Seg l by FINSEQ_1:def 14;
A31: ( rng (Sgm (Seg n)) = Seg n & [:(Seg n),N:] c= Indices A ) by A2, A10, FINSEQ_1:def 14, ZFMISC_1:95;
A32: rng (Sgm N) = N by FINSEQ_1:def 14;
dom (Sgm N) = Seg n by A1, FINSEQ_3:40;
then A33: (Sgm N) . i in N by A28, A32, FUNCT_1:def 3;
A34: j in Seg l by A22, A26, A27, ZFMISC_1:87;
then A35: j = (idseq l) . j by FINSEQ_2:49
.= (Sgm (Seg l)) . j by FINSEQ_3:48 ;
then [((Sgm N) . I),((Sgm (Seg l)) . J)] in Indices X by A2, A21, A34, A33, ZFMISC_1:87;
then A36: [I,J] in Indices B by A16, A32, A30, A25, MATRIX13:17;
A37: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by FINSEQ_1:def 14;
A38: i = (idseq n) . i by A28, FINSEQ_2:49
.= (Sgm (Seg n)) . i by FINSEQ_3:48 ;
then [((Sgm (Seg n)) . i),((Sgm N) . i)] in Indices A by A2, A10, A28, A33, ZFMISC_1:87;
then A39: [I,I] in Indices (1. (K,n)) by A4, A32, A31, MATRIX13:17;
A40: [:((Seg m) \ N),(Seg l):] c= Indices X by A15, A21, ZFMISC_1:95;

A41: now :: thesis:

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

per cases by A42, XBOOLE_0:def 5;

suppose A44: kk in N ; :: thesis:

then consider x being object such that
A45: x in dom (Sgm N) and
A46: (Sgm N) . x = kk by A32, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A45;
[((Sgm (Seg n)) . i),((Sgm N) . x)] in Indices A by A2, A10, A28, A38, A44, A46, ZFMISC_1:87;
then A47: [I,x] in Indices (1. (K,n)) by A4, A32, A31, MATRIX13:17;
A48: (Col (X,j)) . kk = X * (kk,j) by A2, A19, A44, MATRIX_0:def 8;
(Line (A,i)) . ((Sgm N) . x) = A * (I,((Sgm N) . x)) by A2, A5, A44, A46, MATRIX_0:def 7
.= (Segm (A,(Seg n),N)) * (I,x) by A4, A38, A47, MATRIX13:def 1
.= 0. K by A4, A43, A46, A47, MATRIX_1:def 3 ;
hence (mlt ((Line (A,i)),(Col (X,j)))) . kk = (0. K) * (X * (kk,j)) by A2, A5, A18, A44, A46, A48, FVSUM_1:61
.= 0. K ;
:: thesis:

end;

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

then consider x being object such that
A50: x in dom (Sgm ((Seg m) \ N)) and
A51: (Sgm ((Seg m) \ N)) . x = kk by A37, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A50;
A52: (Line (A,i)) . kk = A * (I,((Sgm ((Seg m) \ N)) . x)) by A5, A42, A51, MATRIX_0:def 7;
[((Sgm ((Seg m) \ N)) . x),((Sgm (Seg l)) . J)] in Indices X by A15, A21, A34, A35, A49, A51, ZFMISC_1:87;
then A53: [x,J] in Indices (0. (K,(m -' n),l)) by A17, A30, A37, A40, MATRIX13:17;
(Col (X,j)) . kk = X * (((Sgm ((Seg m) \ N)) . x),((Sgm (Seg l)) . j)) by A15, A19, A35, A49, A51, MATRIX_0:def 8
.= (0. (K,(m -' n),l)) * (x,J) by A17, A53, MATRIX13:def 1
.= 0. K by A53, MATRIX_3:1 ;
hence (mlt ((Line (A,i)),(Col (X,j)))) . kk = (A * (I,((Sgm ((Seg m) \ N)) . x))) * (0. K) by A5, A18, A42, A52, FVSUM_1:61
.= 0. K ;
:: thesis:

end;

A54: (Col (X,j)) . ((Sgm N) . i) = X * (((Sgm N) . i),j) by A2, A19, A33, MATRIX_0:def 8
.= B * (I,J) by A16, A35, A36, MATRIX13:def 1 ;
(Line (A,i)) . ((Sgm N) . i) = A * (I,((Sgm N) . I)) by A2, A5, A33, MATRIX_0:def 7
.= (Segm (A,(Seg n),N)) * (I,I) by A4, A38, A39, MATRIX13:def 1
.= 1_ K by A4, A39, MATRIX_1:def 3 ;
then A55: (mlt ((Line (A,i)),(Col (X,j)))) . ((Sgm N) . i) = (1_ K) * (B * (I,J)) by A2, A5, A18, A33, A54, FVSUM_1:61
.= B * (I,J) ;
AX * (i,j) = (Line (A,i)) "*" (Col (X,j)) by A5, A18, A26, MATRIX_3:def 4
.= Sum (mlt ((Line (A,i)),(Col (X,j)))) ;
hence AX * (i,j) = B * (i,j) by A2, A33, A55, A29, A41, MATRIX_3:12; :: thesis:

end;

then AX = B by MATRIX_0:27;
hence X in Solutions_of (A,B) by A5, A22, A18, A23; :: thesis: