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 in dom p & j in dom p & i <= j holds
for l being Element of 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 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 in dom p & j in dom p & i <= j holds
for l being Element of 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 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 in dom p & j in dom p & i <= j holds
for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . j) . l )
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 in dom p & j in dom p & i <= j holds
for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . j) . l
defpred S₁[ Element of NAT ] means ( $1 in dom p implies for i being Element of NAT st i in dom p & i <= $1 holds
for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . $1) . l );
A2: S₁[ 0 ] ;
A3: for j being Element of NAT st S₁[j] holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A4: ( j in dom p implies for i being Element of NAT st i in dom p & i <= j holds
for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . j) . l ) ; :: thesis: S₁[j + 1]
assume j + 1 in dom p ; :: thesis: for i being Element of NAT st i in dom p & i <= j + 1 holds
for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l
then A5: ( j + 1 >= 1 & j + 1 <= len p ) by FINSEQ_3:27;
then A6: ( j + 1 = 1 or j + 1 > 1 ) by XXREAL_0:1;
let i be Element of NAT ; :: thesis: ( i in dom p & i <= j + 1 implies for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l )
assume A7: ( i in dom p & i <= j + 1 ) ; :: thesis: for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l
i in Seg (len p) by A7, FINSEQ_1:def 3;
then A8: ( i >= 1 & i <= len p ) by FINSEQ_1:3;

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

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

hence for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l by A7, A8, XXREAL_0:1; :: thesis: verum

end;

suppose A9: j >= 1 ; :: thesis: for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l

A10: j < len p by A5, NAT_1:13;
then A11: j in Seg (len p) by A9, FINSEQ_1:3;
then A12: j in dom p by FINSEQ_1:def 3;
thus for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l :: thesis: verum

proof

let l be Element of NAT ; :: thesis: ( l in dom (p . i) implies (p . i) . l = (p . (j + 1)) . l )
assume A13: l in dom (p . i) ; :: thesis: (p . i) . l = (p . (j + 1)) . l

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

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

then A15: dom (p . i) c= dom (p . j) by A1, A7, A12, Th30;
thus (p . i) . l = (p . j) . l by A4, A7, A11, A13, A14, FINSEQ_1:def 3
.= (p . (j + 1)) . l by A1, A9, A10, A13, A15, 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;

for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A2, A3);
hence for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . j) . l ; :: thesis: verum