let D be non empty set ; :: thesis: for M being Matrix of D
for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being Element of NAT st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * i,j = (p . (len M)) . (((i - 1) * (width M)) + j) )
let M be Matrix of D; :: thesis: for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being Element of NAT st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * i,j = (p . (len M)) . (((i - 1) * (width M)) + j) )
let p be FinSequence of D * ; :: thesis: ( len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) implies for i, j being Element of NAT st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * i,j = (p . (len M)) . (((i - 1) * (width M)) + j) ) )
assume A1: ( len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ; :: thesis: for i, j being Element of NAT st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * i,j = (p . (len M)) . (((i - 1) * (width M)) + j) )
let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices M implies ( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * i,j = (p . (len M)) . (((i - 1) * (width M)) + j) ) )
assume A2: [i,j] in Indices M ; :: thesis: ( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * i,j = (p . (len M)) . (((i - 1) * (width M)) + j) )
A3: ( i in Seg (len M) & j in Seg (width M) ) by A2, MATRPROB:12;
then A4: ( i >= 1 & i <= len M ) by FINSEQ_1:3;
A5: i in dom p by A1, A3, FINSEQ_1:def 3;
( len M >= 1 & len M <= len p ) by A1, A3, FINSEQ_1:4, NAT_1:14;
then len M in Seg (len p) by FINSEQ_1:3;
then A6: len M in dom p by FINSEQ_1:def 3;
A7: ( ((i - 1) * (width M)) + j in dom (p . i) & M * i,j = (p . i) . (((i - 1) * (width M)) + j) ) by A1, A2, Th35;
dom (p . i) c= dom (p . (len M)) by A1, A4, A5, A6, Th30;
hence ( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * i,j = (p . (len M)) . (((i - 1) * (width M)) + j) ) by A1, A4, A5, A6, A7, Th33; :: thesis: verum