let k, i be Element of NAT ; :: thesis: for q being FinSubsequence st k in dom (Seq q) holds
ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j )
let q be FinSubsequence; :: thesis: ( k in dom (Seq q) implies ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j ) )
assume A1: k in dom (Seq q) ; :: thesis: ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j )
consider ss being FinSubsequence such that
A2: dom ss = dom q and
A3: rng ss = dom (i Shift q) and
A4: for l being Element of NAT st l in dom q holds
ss . l = i + l and
ss is one-to-one by Th56;
A5: rng (Seq ss) = dom (i Shift q) by A3, Lm6;
A6: rng (Sgm (dom q)) = dom q by FINSEQ_1:50;
A7: dom (Seq q) = dom (q * (Sgm (dom q))) by FINSEQ_1:def 14
.= dom (Sgm (dom q)) by A6, RELAT_1:27 ;
A8: for l1 being Element of NAT st l1 in dom (Seq q) holds
ex j1 being Element of NAT st
( j1 = (Sgm (dom q)) . l1 & (Seq ss) . l1 = i + j1 )

proof

let l1 be Element of NAT ; :: thesis: ( l1 in dom (Seq q) implies ex j1 being Element of NAT st
( j1 = (Sgm (dom q)) . l1 & (Seq ss) . l1 = i + j1 ) )
assume A9: l1 in dom (Seq q) ; :: thesis: ex j1 being Element of NAT st
( j1 = (Sgm (dom q)) . l1 & (Seq ss) . l1 = i + j1 )
A10: (Sgm (dom q)) . l1 in rng (Sgm (dom q)) by A7, A9, FUNCT_1:def 3;
then A11: (Sgm (dom q)) . l1 in dom q by FINSEQ_1:50;
rng (Sgm (dom q)) c= NAT by FINSEQ_1:def 4;
then reconsider j1 = (Sgm (dom q)) . l1 as Element of NAT by A10;
(Seq ss) . l1 = (ss * (Sgm (dom ss))) . l1 by FINSEQ_1:def 14
.= ss . j1 by A2, A7, A9, FUNCT_1:13
.= i + j1 by A4, A11 ;
hence ex j1 being Element of NAT st
( j1 = (Sgm (dom q)) . l1 & (Seq ss) . l1 = i + j1 ) ; :: thesis: verum

end;

A12: rng ss = rng (Sgm (dom (i Shift q))) by A3, FINSEQ_1:50;
rng (Sgm (dom (i Shift q))) c= NAT by FINSEQ_1:def 4;
then rng (Seq ss) c= NAT by A12, Lm6;
then reconsider fs = Seq ss as FinSequence of NAT by FINSEQ_1:def 4;
A13: ex l2 being Nat st dom (i Shift q) c= Seg l2 by FINSEQ_1:def 12;
A14: dom (Seq ss) = dom (ss * (Sgm (dom ss))) by FINSEQ_1:def 14
.= dom (Sgm (dom q)) by A2, A6, RELAT_1:27 ;
for n, m, k1, k2 being natural number st 1 <= n & n < m & m <= len fs & k1 = fs . n & k2 = fs . m holds
k1 < k2

proof

let n, m, k1, k2 be natural number ; :: thesis: ( 1 <= n & n < m & m <= len fs & k1 = fs . n & k2 = fs . m implies k1 < k2 )
assume that
A15: 1 <= n and
A16: n < m and
A17: m <= len fs and
A18: k1 = fs . n and
A19: k2 = fs . m ; :: thesis: k1 < k2
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 12;
A20: dom fs = Seg (len fs) by FINSEQ_1:def 3
.= { l3 where l3 is Element of NAT : ( 1 <= l3 & l3 <= len fs ) } by FINSEQ_1:def 1 ;
n + 1 <= m by A16, INT_1:7;
then n + 1 <= len fs by A17, XXREAL_0:2;
then A21: n <= (len fs) - 1 by XREAL_1:19;
(len fs) + 0 <= (len fs) + 1 by XREAL_1:7;
then (len fs) - 1 <= len fs by XREAL_1:20;
then n <= len fs by A21, XXREAL_0:2;
then A22: n in dom (Seq q) by A7, A14, A15, A20;
1 <= m by A15, A16, XXREAL_0:2;
then A23: m in dom (Seq q) by A7, A14, A17, A20;
consider j2 being Element of NAT such that
A24: j2 = (Sgm (dom q)) . n and
A25: fs . n = i + j2 by A8, A22;
consider j3 being Element of NAT such that
A26: j3 = (Sgm (dom q)) . m and
A27: fs . m = i + j3 by A8, A23;
A28: ex l3 being Nat st dom q c= Seg l3 by FINSEQ_1:def 12;
dom (Seq ss) = Seg (len fs) by FINSEQ_1:def 3;
then len fs = len (Sgm (dom q)) by A14, FINSEQ_1:def 3;
then j2 < j3 by A15, A16, A17, A24, A26, A28, FINSEQ_1:def 13;
hence k1 < k2 by A18, A19, A25, A27, XREAL_1:8; :: thesis: verum

end;

then fs = Sgm (dom (i Shift q)) by A5, A13, FINSEQ_1:def 13;
hence ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j ) by A1, A8; :: thesis: verum