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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being Nat st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being Nat st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) )
let p be FinSequence of D * ; :: thesis: ( 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)) ) implies for i, j being Nat st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) ) )
assume that
A1: len p = len M and
A2: p . 1 = M . 1 and
A3: for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; :: thesis: for i, j being Nat st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) )
let i, j be Nat; :: thesis: ( [i,j] in Indices M implies ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) ) )
assume A4: [i,j] in Indices M ; :: thesis: ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) )
A5: j in Seg (width M) by A4, MATRPROB:12;
i in Seg (len M) by A4, MATRPROB:12;
then A6: i in dom M by FINSEQ_1:def 3;
then A7: i >= 1 by FINSEQ_3:25;
A8: i <= len M by A6, FINSEQ_3:25;

per cases ( i > 1 or i = 1 ) by A7, XXREAL_0:1;

suppose A9: i > 1 ; :: thesis: ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) )

then reconsider ii = i - 1 as Nat by NAT_1:20;
i < (len M) + 1 by A8, NAT_1:13;
then A10: i - 1 < ((len M) + 1) - 1 by XREAL_1:14;
ii + 1 > 1 by A9;
then A11: ii >= 1 by NAT_1:13;
then (p . (ii + 1)) . ((ii * (width M)) + j) = (M . (ii + 1)) . j by A1, A2, A3, A5, A10, Th34;
hence ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) ) by A1, A2, A3, A4, A5, A11, A10, Th34, MATRPROB:14; :: thesis: verum

end;

suppose i = 1 ; :: thesis: ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) )

hence ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) ) by A1, A2, A3, A4, Th31; :: thesis: verum

end;

end;