let D be non empty set ; :: thesis: for M being Matrix of D holds Values M = { (M * (i,j)) where i, j is Nat : [i,j] in Indices M }
let M be Matrix of D; :: thesis: Values M = { (M * (i,j)) where i, j is Nat : [i,j] in Indices M }
set V = { (M * (i,j)) where i, j is 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 Th35;

now :: thesis: for y being object holds
( ( y in Values M implies y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M } ) & ( y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M } implies y in Values M ) )

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

hereby :: thesis: ( y in { (M * (i,j)) where i, j is 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 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:10;
consider i being Nat such that
A8: i in dom M and
A9: M . i = f by A5, FINSEQ_2:10;
reconsider i = i, j = j as Nat ;
A10: [i,j] in Indices M by A8, A9, A6, Th37;
then ex p being FinSequence of D st
( p = M . i & M * (i,j) = p . j ) by Def5;
hence y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M } by A9, A7, A10; :: thesis: verum

end;

assume y in { (M * (i,j)) where i, j is Nat : [i,j] in Indices M } ; :: thesis: y in Values M
then consider i, j being 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, Def5;
j in dom f by A12, A13, Th38;
then A15: f . j in rng f by FUNCT_1:def 3;
i in dom M by A12, ZFMISC_1:87;
then A16: M . i in rng M by FUNCT_1:def 3;
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 Nat : [i,j] in Indices M } by TARSKI:2; :: thesis: verum