let i be Nat; for q being FinSubsequence ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (Shift (q,i)) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one )
let q be FinSubsequence; ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (Shift (q,i)) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one )
consider n being Nat such that
A1:
dom q c= Seg n
by FINSEQ_1:def 12;
defpred S1[ object , object ] means ex k being Element of NAT st
( k = $1 & $2 = i + k );
A2:
for x being object st x in dom q holds
ex y being object st S1[x,y]
consider f being Function such that
A3:
dom f = dom q
and
A4:
for x being object st x in dom q holds
S1[x,f . x]
from CLASSES1:sch 1(A2);
reconsider ss = f as FinSubsequence by A1, A3, FINSEQ_1:def 12;
A5:
dom (Shift (q,i)) = { (k + i) where k is Nat : k in dom q }
by Def12;
A6:
rng ss = dom (Shift (q,i))
A11:
for k being Element of NAT st k in dom q holds
ss . k = i + k
for x1, x2 being object st x1 in dom ss & x2 in dom ss & ss . x1 = ss . x2 holds
x1 = x2
then
ss is one-to-one
;
hence
ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (Shift (q,i)) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one )
by A3, A6, A11; verum