let D be non empty set ; :: thesis: for M being Matrix of D holds Values M = { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M }
let M be Matrix of D; :: thesis: Values M = { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M }
set V = { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } ;
set R = { (rng f) where f is Element of D * : f in rng M } ;
A1: Values M = union { (rng f) where f is Element of D * : f in rng M } by Th3;

now

let y be set ; :: thesis: ( ( y in Values M implies y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } ) & ( y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } implies y in Values M ) )

hereby :: thesis: ( y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } implies y in Values M )

assume y in Values M ; :: thesis: y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M }
then consider Y being set such that
A2: y in Y and
A3: Y in { (rng f) where f is Element of D * : f in rng M } by A1, TARSKI:def 4;
consider f being Element of D * such that
A4: Y = rng f and
A5: f in rng M by A3;
consider j being Nat such that
A6: j in dom f and
A7: f . j = y by A2, A4, FINSEQ_2:11;
consider i being Nat such that
A8: i in dom M and
A9: M . i = f by A5, FINSEQ_2:11;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 13;
A10: [i,j] in Indices M by A8, A9, A6, Th5;
then ex p being FinSequence of D st
( p = M . i & M * i,j = p . j ) by MATRIX_1:def 6;
hence y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } by A9, A7, A10; :: thesis: verum

end;

assume y in { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } ; :: thesis: y in Values M
then consider i, j being Element of NAT such that
A11: y = M * i,j and
A12: [i,j] in Indices M ;
consider f being FinSequence of D such that
A13: f = M . i and
A14: M * i,j = f . j by A12, MATRIX_1:def 6;
j in dom f by A12, A13, Th6;
then A15: f . j in rng f by FUNCT_1:def 5;
Indices M = [:(dom M),(Seg (width M)):] by MATRIX_1:def 5;
then i in dom M by A12, ZFMISC_1:106;
then A16: M . i in rng M by FUNCT_1:def 5;
f in D * by FINSEQ_1:def 11;
then rng f in { (rng f) where f is Element of D * : f in rng M } by A13, A16;
hence y in Values M by A1, A11, A14, A15, TARSKI:def 4; :: thesis: verum

end;

hence Values M = { (M * i,j) where i, j is Element of NAT : [i,j] in Indices M } by TARSKI:2; :: thesis: verum