let i, j be Nat; 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 ; 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; ( [i,j] in Indices M implies M * (i,j) = (M . i) . j )
assume
[i,j] in Indices M
; 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
; verum