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 )
A1: Values M = { (M * i1,j1) where i1, j1 is Element of NAT : [i1,j1] in Indices M } by Th7;
assume ( 1 <= i & i <= len M & 1 <= j & j <= width M ) ; :: thesis: M * i,j in Values M
then [i,j] in Indices M by MATRIX_1:37;
hence M * i,j in Values M by A1; :: thesis: verum