let i be Nat; :: thesis: 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; :: thesis: 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 S₁[ 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 S₁[x,y]

proof

let x be object ; :: thesis: ( x in dom q implies ex y being object st S₁[x,y] )
assume x in dom q ; :: thesis: ex y being object st S₁[x,y]
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 object 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 (Shift (q,i)) = { (k + i) where k is Nat : k in dom q } by Def12;
A6: rng ss = dom (Shift (q,i))

proof

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ss or y in dom (Shift (q,i)) )
assume y in rng ss ; :: thesis: y in dom (Shift (q,i))
then consider x being object such that
A7: x in dom ss and
A8: y = ss . x by FUNCT_1:def 3;
ex k1 being Element of NAT st
( k1 = x & ss . x = i + k1 ) by A3, A4, A7;
hence y in dom (Shift (q,i)) by A3, A5, A7, A8; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (Shift (q,i)) or y in rng ss )
assume y in dom (Shift (q,i)) ; :: thesis: y in rng ss
then consider k2 being Nat such that
A9: y = k2 + i 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 3; :: 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 object st x1 in dom ss & x2 in dom ss & ss . x1 = ss . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: 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 ;
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; :: thesis: verum