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 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: ( 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 A16, A17; :: thesis: X in Solutions_of (A,B)

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;

hence X in Solutions_of (A,B) by A5, A22, A18, A23; :: thesis: verum

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 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: ( 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 A16, A17; :: thesis: X in Solutions_of (A,B)

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: for i, j being Nat st [i,j] in Indices AX holds

AX * (i,j) = B * (i,j)

then
AX = B
by MATRIX_0:27;AX * (i,j) = B * (i,j)

A25:
[:N,(Seg l):] c= Indices X
by A2, A21, ZFMISC_1:95;

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 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 13;

A31: ( rng (Sgm (Seg n)) = Seg n & [:(Seg n),N:] c= Indices A ) by A2, A10, FINSEQ_1:def 13, ZFMISC_1:95;

A32: rng (Sgm N) = N by A2, FINSEQ_1:def 13;

dom (Sgm N) = Seg n by A1, A2, 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 A15, FINSEQ_1:def 13;

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;

.= 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: verum

end;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 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 13;

A31: ( rng (Sgm (Seg n)) = Seg n & [:(Seg n),N:] c= Indices A ) by A2, A10, FINSEQ_1:def 13, ZFMISC_1:95;

A32: rng (Sgm N) = N by A2, FINSEQ_1:def 13;

dom (Sgm N) = Seg n by A1, A2, 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 A15, FINSEQ_1:def 13;

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: for kk being Nat st kk in Seg m & kk <> (Sgm N) . I holds

(mlt ((Line (A,i)),(Col (X,j)))) . kk = 0. K

A54: (Col (X,j)) . ((Sgm N) . i) =
X * (((Sgm N) . i),j)
by A2, A19, A33, MATRIX_0:def 8
(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)))) . b_{1} = 0. K )

assume that

A42: kk in Seg m and

A43: kk <> (Sgm N) . I ; :: thesis: (mlt ((Line (A,i)),(Col (X,j)))) . b_{1} = 0. K

end;assume that

A42: kk in Seg m and

A43: kk <> (Sgm N) . I ; :: thesis: (mlt ((Line (A,i)),(Col (X,j)))) . b

per cases
( kk in N or kk in (Seg m) \ N )
by A42, XBOOLE_0:def 5;

end;

suppose A44:
kk in N
; :: thesis: (mlt ((Line (A,i)),(Col (X,j)))) . b_{1} = 0. K

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: verum

end;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: verum

suppose A49:
kk in (Seg m) \ N
; :: thesis: (mlt ((Line (A,i)),(Col (X,j)))) . b_{1} = 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 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: verum

end;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: verum

.= 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: verum

hence X in Solutions_of (A,B) by A5, A22, A18, A23; :: thesis: verum