let i be Nat; :: thesis:
let k be Element of NAT ; :: thesis:
let q be FinSubsequence; :: thesis:
assume A1: k in dom (Seq q) ; :: thesis:
consider ss being FinSubsequence such that
A2: dom ss = dom q and
A3: rng ss = dom (Shift (q,i)) 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 Th40;
A5: rng (Seq ss) = dom (Shift (q,i)) by A3, FINSEQ_1:101;
A6: rng (Sgm (dom q)) = dom q by FINSEQ_1:50;
A7: dom (Seq q) = dom (q * (Sgm (dom q)))
.= dom (Sgm (dom q)) by A6, RELAT_1:27 ;
A8: for l1 being 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 )

let l1 be Nat; :: thesis:
assume A9: l1 in dom (Seq q) ; :: thesis:
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;
reconsider j1 = (Sgm (dom q)) . l1 as Element of NAT by A10;
(Seq ss) . l1 = (ss * (Sgm (dom ss))) . l1
.= 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:

end;

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

let n, m, k1, k2 be Nat; :: thesis:
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:
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 Nat : ( 1 <= l3 & l3 <= len fs ) } ;
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:

end;