let D be non empty set ; :: thesis: for i, j being Nat
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
M * (i,j) in Values M
let i, j be Nat; :: thesis: for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
M * (i,j) in Values M
let M be Matrix of D; :: thesis: ( 1 <= i & i <= len M & 1 <= j & j <= width M implies M * (i,j) in Values M )
assume ( 1 <= i & i <= len M & 1 <= j & j <= width M ) ; :: thesis: M * (i,j) in Values M
then A1: [i,j] in Indices M by Th30;
Values M = { (M * (i1,j1)) where i1, j1 is Nat : [i1,j1] in Indices M } by Th39;
hence M * (i,j) in Values M by A1; :: thesis: verum