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_0:23;
then A8: width (Segm (B,nt,(Sgm (Seg (width B))))) = width B by FINSEQ_1:57;
let x be object ; :: 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_0:23;
then A13: width (Segm (A,nt,(Sgm (Seg (width A))))) = width A by FINSEQ_1:57;
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 :: thesis: for j, k being Nat st [j,k] in Indices (A * X) holds
(A * X) * (j,k) = B * (j,k)

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:87;
reconsider j9 = j, k9 = k as Element of NAT by ORDINAL1:def 12;
A20: j in dom (A * X) by A18, ZFMISC_1:87;

now :: thesis: (A * X) * (j,k) = B * (j,k)

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:124;
Sgm (Seg (width B)) = idseq (width B) by FINSEQ_3:48;
then A23: (Sgm (Seg (width B))) . k9 = k by A11, A8, A14, A19, FINSEQ_2:49;
consider p being object such that
A24: p in dom nt and
A25: nt . p = j9 by A21, FUNCT_1:def 3;
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_0:23;
then A26: [p,k] in Indices (Segm (B,nt,(Sgm (Seg (width B))))) by A11, A7, A14, A19, A24, A22, ZFMISC_1:87;
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:66
.= (0. K) * (Sum (Col (X,k))) by FVSUM_1:73
.= 0. K
.= (Line (B,j)) . k by A11, A8, A14, A19, A28, FINSEQ_2:57
.= B * (j,k) by A11, A8, A14, A19, MATRIX_0:def 7 ;
:: 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:57, MATRIX_0: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; :: thesis: verum