let i be Element of NAT ; :: thesis: for q being FinSubsequence ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (i Shift q) & ( 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; :: thesis: ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (i Shift q) & ( 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;
A2: Seg n = { k where k is Element of NAT : ( 1 <= k & k <= n ) } by FINSEQ_1:def 1;
defpred S₁[ set , set ] means ex k being Element of NAT st
( k = $1 & $2 = i + k );
A4: for x being set st x in dom q holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in dom q implies ex y being set st S₁[x,y] )
assume x in dom q ; :: thesis: ex y being set st S₁[x,y]
then x in Seg n by A1;
then consider k1 being Element of NAT such that
A5: ( x = k1 & 1 <= k1 & k1 <= n ) by A2;
reconsider x = x as Element of NAT by A5;
take i + x ; :: thesis: S₁[x,i + x]
thus S₁[x,i + x] ; :: thesis: verum

end;

consider f being Function such that
A6: dom f = dom q and
A7: for x being set st x in dom q holds
S₁[x,f . x] from CLASSES1:sch 1(A4);
reconsider ss = f as FinSubsequence by A1, A6, FINSEQ_1:def 12;
A8: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def15;
A9: rng ss = dom (i Shift q)

proof

thus rng ss c= dom (i Shift q) :: according to XBOOLE_0:def 10 :: thesis: dom (i Shift q) c= rng ss

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ss or y in dom (i Shift q) )
assume y in rng ss ; :: thesis: y in dom (i Shift q)
then consider x being set such that
A10: ( x in dom ss & y = ss . x ) by FUNCT_1:def 5;
consider k1 being Element of NAT such that
A11: ( k1 = x & ss . x = i + k1 ) by A6, A7, A10;
thus y in dom (i Shift q) by A6, A8, A10, A11; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (i Shift q) or y in rng ss )
assume y in dom (i Shift q) ; :: thesis: y in rng ss
then consider k2 being Element of NAT such that
A12: ( y = i + k2 & k2 in dom q ) by A8;
consider k3 being Element of NAT such that
A13: ( k3 = k2 & ss . k2 = i + k3 ) by A7, A12;
thus y in rng ss by A6, A12, A13, FUNCT_1:def 5; :: thesis: verum

end;

A14: for k being Element of NAT st k in dom q holds
ss . k = i + k

proof

let k be Element of NAT ; :: thesis: ( k in dom q implies ss . k = i + k )
assume k in dom q ; :: thesis: ss . k = i + k
then consider k1 being Element of NAT such that
A15: ( k1 = k & ss . k = i + k1 ) by A7;
thus ss . k = i + k by A15; :: thesis: verum

end;

ss is one-to-one

proof

for x1, x2 being set st x1 in dom ss & x2 in dom ss & ss . x1 = ss . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom ss & x2 in dom ss & ss . x1 = ss . x2 implies x1 = x2 )
assume A16: ( x1 in dom ss & x2 in dom ss & ss . x1 = ss . x2 ) ; :: thesis: x1 = x2
then consider k1 being Element of NAT such that
A17: ( k1 = x1 & ss . x1 = i + k1 ) by A6, A7;
consider k2 being Element of NAT such that
A18: ( k2 = x2 & ss . x2 = i + k2 ) by A6, A7, A16;
thus x1 = x2 by A16, A17, A18; :: thesis: verum

end;

hence ss is one-to-one by FUNCT_1:def 8; :: thesis: verum

end;

hence ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (i Shift q) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one ) by A6, A9, A14; :: thesis: verum