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 in dom p & j in dom p & i <= j holds
for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . j) . 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 i, j being Nat st i in dom p & j in dom p & i <= j holds
for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . j) . 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 i, j being Nat st i in dom p & j in dom p & i <= j holds
for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . j) . 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 i, j being Nat st i in dom p & j in dom p & i <= j holds
for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . j) . l
defpred S₁[ Nat] means ( $1 in dom p implies for i being Nat st i in dom p & i <= $1 holds
for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . $1) . l );
A4: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A5: ( j in dom p implies for i being Nat st i in dom p & i <= j holds
for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . j) . l ) ; :: thesis: S₁[j + 1]
assume A6: j + 1 in dom p ; :: thesis: for i being Nat st i in dom p & i <= j + 1 holds
for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l
then A7: j + 1 <= len p by FINSEQ_3:25;
j + 1 >= 1 by A6, FINSEQ_3:25;
then A8: ( j + 1 = 1 or j + 1 > 1 ) by XXREAL_0:1;
let i be Nat; :: thesis: ( i in dom p & i <= j + 1 implies for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l )
assume that
A9: i in dom p and
A10: i <= j + 1 ; :: thesis: for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l
i in Seg (len p) by A9, FINSEQ_1:def 3;
then A11: i >= 1 by FINSEQ_1:1;

per cases ( j + 1 = 1 or j >= 1 ) by A8, NAT_1:13;

suppose j + 1 = 1 ; :: thesis: for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l

hence for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l by A10, A11, XXREAL_0:1; :: thesis: verum

end;

suppose A12: j >= 1 ; :: thesis: for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l

A13: j < len p by A7, NAT_1:13;
then A14: j in Seg (len p) by A12, FINSEQ_1:1;
then A15: j in dom p by FINSEQ_1:def 3;
thus for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l :: thesis: verum

proof

let l be Nat; :: thesis: ( l in dom (p . i) implies (p . i) . l = (p . (j + 1)) . l )
assume A16: l in dom (p . i) ; :: thesis: (p . i) . l = (p . (j + 1)) . l

per cases ( i <= j or i = j + 1 ) by A10, NAT_1:8;

suppose A17: i <= j ; :: thesis: (p . i) . l = (p . (j + 1)) . l

then A18: dom (p . i) c= dom (p . j) by A1, A2, A3, A9, A15, Th30;
thus (p . i) . l = (p . j) . l by A5, A9, A14, A16, A17, FINSEQ_1:def 3
.= (p . (j + 1)) . l by A1, A3, A12, A13, A16, A18, Th32 ; :: thesis: verum

end;

suppose i = j + 1 ; :: thesis: (p . i) . l = (p . (j + 1)) . l

hence (p . i) . l = (p . (j + 1)) . l ; :: thesis: verum

end;

end;

end;

end;

end;

end;

A19: S₁[ 0 ] ;
for j being Nat holds S₁[j] from NAT_1:sch 2(A19, A4);
hence for i, j being Nat st i in dom p & j in dom p & i <= j holds
for l being Nat st l in dom (p . i) holds
(p . i) . l = (p . j) . l ; :: thesis: verum