let D be non empty set ; :: thesis: for M being Matrix of D
for i, j being Nat st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) )
let M be Matrix of D; :: thesis: for i, j being Nat st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) )
let i, j be Nat; :: thesis: ( [i,j] in Indices M implies ( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) ) )
assume A1: [i,j] in Indices M ; :: thesis: ( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) )
Seg (len M) <> {} by A1, MATRPROB:12;
then len M <> 0 ;
then ex p being FinSequence of D * st
( Mx2FinS M = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) by Def5;
hence ( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) ) by A1, Th36; :: thesis: verum