let i, j be Element of NAT ; :: thesis: for D being non empty set
for M being Matrix of D st [i,j] in Indices M holds
M * i,j = (M . i) . j
let D be non empty set ; :: thesis: for M being Matrix of D st [i,j] in Indices M holds
M * i,j = (M . i) . j
let M be Matrix of D; :: thesis: ( [i,j] in Indices M implies M * i,j = (M . i) . j )
assume [i,j] in Indices M ; :: thesis: M * i,j = (M . i) . j
then consider p being FinSequence of D such that
A1: ( p = M . i & M * i,j = p . j ) by MATRIX_1:def 6;
thus M * i,j = (M . i) . j by A1; :: thesis: verum