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 j being Nat st j >= 1 & j < len p holds
for l being Nat st l in Seg (width M) holds
( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l )
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 j being Nat st j >= 1 & j < len p holds
for l being Nat st l in Seg (width M) holds
( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l )
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 j being Nat st j >= 1 & j < len p holds
for l being Nat st l in Seg (width M) holds
( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l ) )
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 j being Nat st j >= 1 & j < len p holds
for l being Nat st l in Seg (width M) holds
( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l )
let j be Nat; :: thesis: ( j >= 1 & j < len p implies for l being Nat st l in Seg (width M) holds
( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l ) )
assume that
A4: j >= 1 and
A5: j < len p ; :: thesis: for l being Nat st l in Seg (width M) holds
( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l )
A6: j + 1 >= 1 by A4, NAT_1:13;
j in Seg (len p) by A4, A5, FINSEQ_1:1;
then j in dom p by FINSEQ_1:def 3;
then A7: len (p . j) = j * (width M) by A1, A2, A3, Th29;
let l be Nat; :: thesis: ( l in Seg (width M) implies ( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l ) )
assume A8: l in Seg (width M) ; :: thesis: ( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l )
A9: l <= width M by A8, FINSEQ_1:1;
j + 1 <= len M by A1, A5, NAT_1:13;
then j + 1 in Seg (len M) by A6, FINSEQ_1:1;
then A10: j + 1 in dom M by FINSEQ_1:def 3;
then A11: l in dom (M . (j + 1)) by A8, Th18;
l >= 1 by A8, FINSEQ_1:1;
then A12: (j * (width M)) + l >= 0 + 1 by XREAL_1:7;
dom p = dom M by A1, FINSEQ_3:29;
then len (p . (j + 1)) = (j + 1) * (width M) by A1, A2, A3, A10, Th29
.= (j * (width M)) + (width M) ;
then (j * (width M)) + l <= len (p . (j + 1)) by A9, XREAL_1:7;
then (j * (width M)) + l in Seg (len (p . (j + 1))) by A12, FINSEQ_1:1;
hence (j * (width M)) + l in dom (p . (j + 1)) by FINSEQ_1:def 3; :: thesis: (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l
p . (j + 1) = (p . j) ^ (M . (j + 1)) by A1, A3, A4, A5;
hence (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l by A11, A7, FINSEQ_1:def 7; :: thesis: verum