let i, j be 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 ex p being FinSequence of D st
( p = M . i & M * (i,j) = p . j ) by MATRIX_0:def 5;
hence M * (i,j) = (M . i) . j ; :: thesis: verum