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;
defpred S₁[ set , set ] means ex k being Element of NAT st
( k = $1 & $2 = i + k );
A2: 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 reconsider x = x as Element of NAT ;
take i + x ; :: thesis: S₁[x,i + x]
thus S₁[x,i + x] ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = dom q and
A4: for x being set st x in dom q holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
reconsider ss = f as FinSubsequence by A1, A3, FINSEQ_1:def 12;
A5: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def15;
A6: 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
A7: x in dom ss and
A8: y = ss . x by FUNCT_1:def 5;
ex k1 being Element of NAT st
( k1 = x & ss . x = i + k1 ) by A3, A4, A7;
hence y in dom (i Shift q) by A3, A5, A7, A8; :: 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
A9: y = i + k2 and
A10: k2 in dom q by A5;
ex k3 being Element of NAT st
( k3 = k2 & ss . k2 = i + k3 ) by A4, A10;
hence y in rng ss by A3, A9, A10, FUNCT_1:def 5; :: thesis: verum

end;

A11: 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 ex k1 being Element of NAT st
( k1 = k & ss . k = i + k1 ) by A4;
hence ss . k = i + k ; :: thesis: verum

end;

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 that
A12: x1 in dom ss and
A13: x2 in dom ss and
A14: ss . x1 = ss . x2 ; :: thesis: x1 = x2
A15: ex k1 being Element of NAT st
( k1 = x1 & ss . x1 = i + k1 ) by A3, A4, A12;
ex k2 being Element of NAT st
( k2 = x2 & ss . x2 = i + k2 ) by A3, A4, A13;
hence x1 = x2 by A14, A15; :: thesis: verum

end;

then ss is one-to-one by FUNCT_1:def 8;
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 A3, A6, A11; :: thesis: verum