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 & n > 0 holds
Solutions_of A,B c= 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 & n > 0 holds
Solutions_of A,B c= 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 & n > 0 holds
Solutions_of A,B c= 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 & n > 0 implies Solutions_of A,B c= 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: n > 0 ; :: thesis: Solutions_of A,B c= Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B))))
set SA = Segm A,nt,(Sgm (Seg (width A)));
A3: len (Segm A,nt,(Sgm (Seg (width A)))) = n by A2, MATRIX_1:24;
width (Segm A,nt,(Sgm (Seg (width A)))) = card (Seg (width A)) by A2, MATRIX_1:24;
then A4: width (Segm A,nt,(Sgm (Seg (width A)))) = width A by FINSEQ_1:78;
set SB = Segm B,nt,(Sgm (Seg (width B)));
A5: len (Segm B,nt,(Sgm (Seg (width B)))) = n by A2, MATRIX_1:24;
width (Segm B,nt,(Sgm (Seg (width B)))) = card (Seg (width B)) by A2, MATRIX_1:24;
then A6: 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 A,B or x in Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B)))) )
assume A7: x in Solutions_of A,B ; :: thesis: x in Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B))))
consider X being Matrix of K such that
A8: x = X and
A9: len X = width A and
A10: width X = width B and
A11: A * X = B by A7;
set SX = (Segm A,nt,(Sgm (Seg (width A)))) * X;
A12: len A = len B by A7, Th33;

A13: now

A14: len ((Segm A,nt,(Sgm (Seg (width A)))) * X) = len (Segm A,nt,(Sgm (Seg (width A)))) by A9, A4, MATRIX_3:def 4;
let j, k be Nat; :: thesis: ( [j,k] in Indices ((Segm A,nt,(Sgm (Seg (width A)))) * X) implies ((Segm A,nt,(Sgm (Seg (width A)))) * X) * j,k = (Segm B,nt,(Sgm (Seg (width B)))) * j,k )
assume A15: [j,k] in Indices ((Segm A,nt,(Sgm (Seg (width A)))) * X) ; :: thesis: ((Segm A,nt,(Sgm (Seg (width A)))) * X) * j,k = (Segm B,nt,(Sgm (Seg (width B)))) * j,k
j in dom ((Segm A,nt,(Sgm (Seg (width A)))) * X) by A15, ZFMISC_1:106;
then A16: j in Seg n by A3, A14, FINSEQ_1:def 3;
width ((Segm A,nt,(Sgm (Seg (width A)))) * X) = width X by A9, A4, MATRIX_3:def 4;
then A17: k in Seg (width B) by A10, A15, ZFMISC_1:106;
dom nt = Seg n by FINSEQ_2:144;
then nt . j in rng nt by A16, FUNCT_1:def 5;
then A18: nt . j in dom A by A1;
dom A = Seg (len B) by A12, FINSEQ_1:def 3;
then nt . j in dom B by A18, FINSEQ_1:def 3;
then A19: [(nt . j),k] in Indices B by A17, ZFMISC_1:106;
reconsider j9 = j, k9 = k as Element of NAT by ORDINAL1:def 13;
Sgm (Seg (width B)) = idseq (width B) by FINSEQ_3:54;
then A20: (Sgm (Seg (width B))) . k9 = k by A17, FINSEQ_2:57;
j in dom (Segm B,nt,(Sgm (Seg (width B)))) by A5, A16, FINSEQ_1:def 3;
then A21: [j,k] in Indices (Segm B,nt,(Sgm (Seg (width B)))) by A6, A17, ZFMISC_1:106;
Line (Segm A,nt,(Sgm (Seg (width A)))),j = Line A,(nt . j) by A16, Lm6;
hence ((Segm A,nt,(Sgm (Seg (width A)))) * X) * j,k = (Line A,(nt . j)) "*" (Col X,k) by A9, A4, A15, MATRIX_3:def 4
.= B * (nt . j9),k by A9, A11, A19, MATRIX_3:def 4
.= (Segm B,nt,(Sgm (Seg (width B)))) * j,k by A21, A20, MATRIX13:def 1 ;
:: thesis: verum

end;

( len ((Segm A,nt,(Sgm (Seg (width A)))) * X) = len (Segm A,nt,(Sgm (Seg (width A)))) & width ((Segm A,nt,(Sgm (Seg (width A)))) * X) = width X ) by A9, A4, MATRIX_3:def 4;
then (Segm A,nt,(Sgm (Seg (width A)))) * X = Segm B,nt,(Sgm (Seg (width B))) by A10, A3, A5, A6, A13, MATRIX_1:21;
hence x in Solutions_of (Segm A,nt,(Sgm (Seg (width A)))),(Segm B,nt,(Sgm (Seg (width B)))) by A8, A9, A10, A4, A6; :: thesis: verum