let i, j be Element of NAT ; :: thesis: for D being non empty set
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 D be non empty set ; :: 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 MATRIX_1:36;
Values M = { (M * (i1,j1)) where i1, j1 is Element of NAT : [i1,j1] in Indices M } by Th7;
hence M * (i,j) in Values M by A1; :: thesis: verum