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_0:23;
width (Segm (A,nt,(Sgm (Seg (width A))))) = card (Seg (width A)) by A2, MATRIX_0:23;
then A4: width (Segm (A,nt,(Sgm (Seg (width A))))) = width A by FINSEQ_1:57;
set SB = Segm (B,nt,(Sgm (Seg (width B))));
A5: len (Segm (B,nt,(Sgm (Seg (width B))))) = n by A2, MATRIX_0:23;
width (Segm (B,nt,(Sgm (Seg (width B))))) = card (Seg (width B)) by A2, MATRIX_0:23;
then A6: 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 (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 :: thesis: for j, k being Nat st [j,k] in Indices ((Segm (A,nt,(Sgm (Seg (width A))))) * X) holds
((Segm (A,nt,(Sgm (Seg (width A))))) * X) * (j,k) = (Segm (B,nt,(Sgm (Seg (width B))))) * (j,k)

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:87;
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:87;
dom nt = Seg n by FINSEQ_2:124;
then nt . j in rng nt by A16, FUNCT_1:def 3;
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:87;
reconsider j9 = j, k9 = k as Element of NAT by ORDINAL1:def 12;
Sgm (Seg (width B)) = idseq (width B) by FINSEQ_3:48;
then A20: (Sgm (Seg (width B))) . k9 = k by A17, FINSEQ_2:49;
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:87;
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_0: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