let l, m, n be Nat; :: thesis: for K being Field
for A being Matrix of n,m,K
for B being Matrix of n,l,K
for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & n > 0 & Segm (A,(Seg n),N) = 1. (K,n) holds
ex X being Matrix of m,l,K st
( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) & Segm (X,N,(Seg l)) = B & X in Solutions_of (A,B) )

let K be Field; :: thesis: for A being Matrix of n,m,K
for B being Matrix of n,l,K
for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & n > 0 & Segm (A,(Seg n),N) = 1. (K,n) holds
ex X being Matrix of m,l,K st
( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) & Segm (X,N,(Seg l)) = B & X in Solutions_of (A,B) )

let A be Matrix of n,m,K; :: thesis: for B being Matrix of n,l,K
for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & n > 0 & Segm (A,(Seg n),N) = 1. (K,n) holds
ex X being Matrix of m,l,K st
( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) & Segm (X,N,(Seg l)) = B & X in Solutions_of (A,B) )

let B be Matrix of n,l,K; :: thesis: for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & n > 0 & Segm (A,(Seg n),N) = 1. (K,n) holds
ex X being Matrix of m,l,K st
( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) & Segm (X,N,(Seg l)) = B & X in Solutions_of (A,B) )

let N be finite without_zero Subset of NAT; :: thesis: ( card N = n & N c= Seg m & n > 0 & Segm (A,(Seg n),N) = 1. (K,n) implies ex X being Matrix of m,l,K st
( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) & Segm (X,N,(Seg l)) = B & X in Solutions_of (A,B) ) )

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: ex X being Matrix of m,l,K st
( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) & Segm (X,N,(Seg l)) = B & X in Solutions_of (A,B) )

A5: width A = m by ;
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 ;
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 ;
A11: n <= card (Seg m) by ;
then A12: ( len (0. (K,m,l)) = m & width (0. (K,m,l)) = l ) by ;
A13: Indices (0. (K,m,l)) = [:(Seg m),(Seg l):] by ;
then A14: [:N,(Seg l):] c= Indices (0. (K,m,l)) by ;
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 ;
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 () \ ([: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 ;
then A19: dom X = Seg m by FINSEQ_1:def 3;
len A = n by ;
then A20: len (A * X) = n by ;
take X ; :: thesis: ( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) & Segm (X,N,(Seg l)) = B & X in Solutions_of (A,B) )
thus ( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) & Segm (X,N,(Seg l)) = B ) by ; :: thesis: X in Solutions_of (A,B)
A21: Indices X = [:(Seg m),(Seg l):] by ;
A22: width B = l by ;
A23: width X = l by ;
then width (A * X) = l by ;
then reconsider AX = A * X as Matrix of n,l,K by ;
A24: Indices B = [:(Seg n),(Seg l):] by ;
now :: thesis: for i, j being Nat st [i,j] in Indices AX holds
AX * (i,j) = B * (i,j)
A25: [:N,(Seg l):] c= Indices X by ;
let i, j be Nat; :: thesis: ( [i,j] in Indices AX implies AX * (i,j) = B * (i,j) )
assume A26: [i,j] in Indices AX ; :: thesis: AX * (i,j) = B * (i,j)
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 ;
( len (Line (A,i)) = m & len (Col (X,j)) = m ) by ;
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 13;
A31: ( rng (Sgm (Seg n)) = Seg n & [:(Seg n),N:] c= Indices A ) by ;
A32: rng (Sgm N) = N by ;
dom (Sgm N) = Seg n by ;
then A33: (Sgm N) . i in N by ;
A34: j in Seg l by ;
then A35: j = () . 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 ;
then A36: [I,J] in Indices B by ;
A37: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by ;
A38: i = () . i by
.= (Sgm (Seg n)) . i by FINSEQ_3:48 ;
then [((Sgm (Seg n)) . i),((Sgm N) . i)] in Indices A by ;
then A39: [I,I] in Indices (1. (K,n)) by ;
A40: [:((Seg m) \ N),(Seg l):] c= Indices X by ;
A41: now :: thesis: for kk being Nat st kk in Seg m & kk <> (Sgm N) . I holds
(mlt ((Line (A,i)),(Col (X,j)))) . kk = 0. K
let kk be Nat; :: thesis: ( kk in Seg m & kk <> (Sgm N) . I implies (mlt ((Line (A,i)),(Col (X,j)))) . b1 = 0. K )
assume that
A42: kk in Seg m and
A43: kk <> (Sgm N) . I ; :: thesis: (mlt ((Line (A,i)),(Col (X,j)))) . b1 = 0. K
per cases ( kk in N or kk in (Seg m) \ N ) by ;
suppose A44: kk in N ; :: thesis: (mlt ((Line (A,i)),(Col (X,j)))) . b1 = 0. K
then consider x being object such that
A45: x in dom (Sgm N) and
A46: (Sgm N) . x = kk by ;
reconsider x = x as Element of NAT by A45;
[((Sgm (Seg n)) . i),((Sgm N) . x)] in Indices A by ;
then A47: [I,x] in Indices (1. (K,n)) by ;
A48: (Col (X,j)) . kk = X * (kk,j) 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)),(Col (X,j)))) . kk = (0. K) * (X * (kk,j)) by
.= 0. K ;
:: thesis: verum
end;
suppose A49: kk in (Seg m) \ N ; :: thesis: (mlt ((Line (A,i)),(Col (X,j)))) . b1 = 0. K
then consider x being object such that
A50: x in dom (Sgm ((Seg m) \ N)) and
A51: (Sgm ((Seg m) \ N)) . x = kk by ;
reconsider x = x as Element of NAT by A50;
A52: (Line (A,i)) . kk = A * (I,((Sgm ((Seg m) \ N)) . x)) by ;
[((Sgm ((Seg m) \ N)) . x),((Sgm (Seg l)) . J)] in Indices X by ;
then A53: [x,J] in Indices (0. (K,(m -' n),l)) by ;
(Col (X,j)) . kk = X * (((Sgm ((Seg m) \ N)) . x),((Sgm (Seg l)) . j)) by
.= (0. (K,(m -' n),l)) * (x,J) by
.= 0. K by ;
hence (mlt ((Line (A,i)),(Col (X,j)))) . kk = (A * (I,((Sgm ((Seg m) \ N)) . x))) * (0. K) by
.= 0. K ;
:: thesis: verum
end;
end;
end;
A54: (Col (X,j)) . ((Sgm N) . i) = X * (((Sgm N) . i),j) by
.= B * (I,J) by ;
(Line (A,i)) . ((Sgm N) . i) = A * (I,((Sgm N) . I)) by
.= (Segm (A,(Seg n),N)) * (I,I) by
.= 1_ K by ;
then A55: (mlt ((Line (A,i)),(Col (X,j)))) . ((Sgm N) . i) = (1_ K) * (B * (I,J)) by
.= B * (I,J) ;
AX * (i,j) = (Line (A,i)) "*" (Col (X,j)) by
.= Sum (mlt ((Line (A,i)),(Col (X,j)))) ;
hence AX * (i,j) = B * (i,j) by ; :: thesis: verum
end;
then AX = B by MATRIX_0:27;
hence X in Solutions_of (A,B) by A5, A22, A18, A23; :: thesis: verum