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) = () |-> (0. K) & Line (B,i) = () |-> (0. K) ) ) holds
Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ())))))

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) = () |-> (0. K) & Line (B,i) = () |-> (0. K) ) ) holds
Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ())))))

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) = () |-> (0. K) & Line (B,i) = () |-> (0. K) ) ) holds
Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ())))))

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) = () |-> (0. K) & Line (B,i) = () |-> (0. K) ) ) implies Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ()))))) )

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) = () |-> (0. K) & Line (B,i) = () |-> (0. K) ) ; :: thesis: Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ())))))
set SB = Segm (B,nt,(Sgm (Seg ())));
set SA = Segm (A,nt,(Sgm (Seg ())));
A5: Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ()))))) c= Solutions_of (A,B)
proof
A6: Seg (len A) = dom B by ;
A7: width (Segm (B,nt,(Sgm (Seg ())))) = card (Seg ()) by ;
then A8: width (Segm (B,nt,(Sgm (Seg ())))) = 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 ())))),(Segm (B,nt,(Sgm (Seg ()))))) or x in Solutions_of (A,B) )
assume x in Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ()))))) ; :: 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 ())))) and
A11: width X = width (Segm (B,nt,(Sgm (Seg ())))) and
A12: (Segm (A,nt,(Sgm (Seg ())))) * X = Segm (B,nt,(Sgm (Seg ()))) ;
set AX = A * X;
width (Segm (A,nt,(Sgm (Seg ())))) = card (Seg ()) by ;
then A13: width (Segm (A,nt,(Sgm (Seg ())))) = width A by FINSEQ_1:57;
then A14: width (A * X) = width X by ;
A15: len (A * X) = len A by ;
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 ;
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 ;
reconsider j9 = j, k9 = k as Element of NAT by ORDINAL1:def 12;
A20: j in dom (A * X) by ;
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 ()) = idseq () by FINSEQ_3:48;
then A23: (Sgm (Seg ())) . k9 = k by ;
consider p being object such that
A24: p in dom nt and
A25: nt . p = j9 by ;
reconsider p = p as Element of NAT by A24;
Indices (Segm (B,nt,(Sgm (Seg ())))) = [:(Seg n),(Seg (card (Seg ()))):] by ;
then A26: [p,k] in Indices (Segm (B,nt,(Sgm (Seg ())))) by ;
Line ((Segm (A,nt,(Sgm (Seg ())))),p) = Line (A,j9) by A24, A25, A22, Lm6;
hence (A * X) * (j,k) = (Line ((Segm (A,nt,(Sgm (Seg ())))),p)) "*" (Col (X,k)) by
.= (Segm (B,nt,(Sgm (Seg ())))) * (p,k9) by
.= B * (j,k) by ;
:: 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 ;
then A28: Line (B,j) = () |-> (0. K) by A4;
Line (A,j) = () |-> (0. K) by ;
hence (A * X) * (j,k) = (() |-> (0. K)) "*" (Col (X,k)) by
.= Sum ((0. K) * (Col (X,k))) by
.= (0. K) * (Sum (Col (X,k))) by FVSUM_1:73
.= 0. K
.= (Line (B,j)) . k by
.= B * (j,k) by ;
:: thesis: verum
end;
end;
end;
hence (A * X) * (j,k) = B * (j,k) ; :: thesis: verum
end;
len (A * X) = len B by ;
then A * X = B by ;
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 ())))),(Segm (B,nt,(Sgm (Seg ()))))) by A1, A3, Th42;
hence Solutions_of (A,B) = Solutions_of ((Segm (A,nt,(Sgm (Seg ())))),(Segm (B,nt,(Sgm (Seg ()))))) by A5; :: thesis: verum