let n be Nat; :: thesis: for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line A,i = (width A) |-> (0. K) & Line B,i = (width B) |-> (0. K) ) ) holds
Solutions_of A,B = Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B))))
let K be Field; :: thesis: for A, B being Matrix of K
for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line A,i = (width A) |-> (0. K) & Line B,i = (width B) |-> (0. K) ) ) holds
Solutions_of A,B = Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B))))
let A, B be Matrix of K; :: thesis: for nt being Element of n -tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line A,i = (width A) |-> (0. K) & Line B,i = (width B) |-> (0. K) ) ) holds
Solutions_of A,B = Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B))))
let nt be Element of n -tuples_on NAT ; :: thesis: ( rng nt c= dom A & dom A = dom B & n > 0 & ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line A,i = (width A) |-> (0. K) & Line B,i = (width B) |-> (0. K) ) ) implies Solutions_of A,B = Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B)))) )
assume that
A1: rng nt c= dom A and
A2: dom A = dom B and
A3: n > 0 and
A4: for i being Nat st i in (dom A) \ (rng nt) holds
( Line A,i = (width A) |-> (0. K) & Line B,i = (width B) |-> (0. K) ) ; :: thesis: Solutions_of A,B = Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B))))
set SB = Segm B,nt,(Sgm (Seg (width B)));
set SA = Segm A,nt,(Sgm (Seg (width A)));
A5: Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B)))) c= Solutions_of A,B

proof

A6: Seg (len A) = dom B by A2, FINSEQ_1:def 3;
A7: width (Segm B,nt,(Sgm (Seg (width B)))) = card (Seg (width B)) by A3, MATRIX_1:24;
then A8: width (Segm B,nt,(Sgm (Seg (width B)))) = width B by FINSEQ_1:78;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B)))) or x in Solutions_of A,B )
assume x in Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B)))) ; :: thesis: x in Solutions_of A,B
then consider X being Matrix of K such that
A9: x = X and
A10: len X = width (Segm A,nt,(Sgm (Seg (width A)))) and
A11: width X = width (Segm B,nt,(Sgm (Seg (width B)))) and
A12: (Segm A,nt,(Sgm (Seg (width A)))) * X = Segm B,nt,(Sgm (Seg (width B))) ;
set AX = A * X;
width (Segm A,nt,(Sgm (Seg (width A)))) = card (Seg (width A)) by A3, MATRIX_1:24;
then A13: width (Segm A,nt,(Sgm (Seg (width A)))) = width A by FINSEQ_1:78;
then A14: width (A * X) = width X by A10, MATRIX_3:def 4;
A15: len (A * X) = len A by A10, A13, MATRIX_3:def 4;

A16: now

A17: dom (A * X) = Seg (len A) by A15, FINSEQ_1:def 3;
let j, k be Nat; :: thesis: ( [j,k] in Indices (A * X) implies (A * X) * j,k = B * j,k )
assume A18: [j,k] in Indices (A * X) ; :: thesis: (A * X) * j,k = B * j,k
A19: k in Seg (width (A * X)) by A18, ZFMISC_1:106;
reconsider j9 = j, k9 = k as Element of NAT by ORDINAL1:def 13;
A20: j in dom (A * X) by A18, ZFMISC_1:106;

now

per cases ( j9 in rng nt or not j9 in rng nt ) ;

suppose A21: j9 in rng nt ; :: thesis: (A * X) * j,k = B * j,k

A22: dom nt = Seg n by FINSEQ_2:144;
Sgm (Seg (width B)) = idseq (width B) by FINSEQ_3:54;
then A23: (Sgm (Seg (width B))) . k9 = k by A11, A8, A14, A19, FINSEQ_2:57;
consider p being set such that
A24: p in dom nt and
A25: nt . p = j9 by A21, FUNCT_1:def 5;
reconsider p = p as Element of NAT by A24;
Indices (Segm B,nt,(Sgm (Seg (width B)))) = [:(Seg n),(Seg (card (Seg (width B)))):] by A3, MATRIX_1:24;
then A26: [p,k] in Indices (Segm B,nt,(Sgm (Seg (width B)))) by A11, A7, A14, A19, A24, A22, ZFMISC_1:106;
Line (Segm A,nt,(Sgm (Seg (width A)))),p = Line A,j9 by A24, A25, A22, Lm6;
hence (A * X) * j,k = (Line (Segm A,nt,(Sgm (Seg (width A)))),p) "*" (Col X,k) by A10, A13, A18, MATRIX_3:def 4
.= (Segm B,nt,(Sgm (Seg (width B)))) * p,k9 by A10, A12, A26, MATRIX_3:def 4
.= B * j,k by A25, A26, A23, MATRIX13:def 1 ;
:: thesis: verum

end;

suppose not j9 in rng nt ; :: thesis: (A * X) * j,k = B * j,k

then A27: j9 in (dom A) \ (rng nt) by A2, A6, A20, A17, XBOOLE_0:def 5;
then A28: Line B,j = (width B) |-> (0. K) by A4;
Line A,j = (width A) |-> (0. K) by A4, A27;
hence (A * X) * j,k = ((width A) |-> (0. K)) "*" (Col X,k) by A10, A13, A18, MATRIX_3:def 4
.= Sum ((0. K) * (Col X,k)) by A10, A13, FVSUM_1:80
.= (0. K) * (Sum (Col X,k)) by FVSUM_1:92
.= 0. K by VECTSP_1:36
.= (Line B,j) . k by A11, A8, A14, A19, A28, FINSEQ_2:71
.= B * j,k by A11, A8, A14, A19, MATRIX_1:def 8 ;
:: thesis: verum

end;

end;

end;

hence (A * X) * j,k = B * j,k ; :: thesis: verum

end;

len (A * X) = len B by A15, A6, FINSEQ_1:def 3;
then A * X = B by A11, A7, A14, A16, FINSEQ_1:78, MATRIX_1:21;
hence x in Solutions_of A,B by A9, A10, A11, A13, A8; :: thesis: verum

end;

Solutions_of A,B c= Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B)))) by A1, A3, Th42;
hence Solutions_of A,B = Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B)))) by A5, XBOOLE_0:def 10; :: thesis: verum