let D be non empty set ; 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; 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; ( 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 )
; 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; verum