consider K being Nat such that
A1: dom p c= Seg K by FINSEQ_1:def 12;
defpred S₁[ set , set ] means ex k being Element of NAT st
( $1 = i + k & $2 = p . k );
A2: for x being set st x in { (i + k) where k is Element of NAT : k in dom p } holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in { (i + k) where k is Element of NAT : k in dom p } implies ex y being set st S₁[x,y] )
assume x in { (i + k) where k is Element of NAT : k in dom p } ; :: thesis: ex y being set st S₁[x,y]
then consider k being Element of NAT such that
A3: x = i + k and
A4: k in dom p ;
[k,(p . k)] in p by A4, FUNCT_1:def 2;
hence ex y being set st S₁[x,y] by A3; :: thesis: verum

end;

consider f being Function such that
A5: dom f = { (i + k) where k is Element of NAT : k in dom p } and
A6: for x being set st x in { (i + k) where k is Element of NAT : k in dom p } holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
{ (i + k) where k is Element of NAT : k in dom p } c= Seg (i + K)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (i + k) where k is Element of NAT : k in dom p } or x in Seg (i + K) )
assume x in { (i + k) where k is Element of NAT : k in dom p } ; :: thesis: x in Seg (i + K)
then consider k being Element of NAT such that
A7: x = i + k and
A8: k in dom p ;
A9: i + k >= k by NAT_1:11;
A10: k >= 1 by A1, A8, FINSEQ_1:1;
A11: k <= K by A1, A8, FINSEQ_1:1;
A12: i + k >= 1 by A9, A10, XXREAL_0:2;
i + k <= i + K by A11, XREAL_1:6;
hence x in Seg (i + K) by A7, A12, FINSEQ_1:1; :: thesis: verum

end;

then reconsider f = f as FinSubsequence by A5, FINSEQ_1:def 12;
take f ; :: thesis: ( dom f = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
f . (i + j) = p . j ) )
thus dom f = { (i + k) where k is Element of NAT : k in dom p } by A5; :: thesis: for j being Nat st j in dom p holds
f . (i + j) = p . j
let j be Nat; :: thesis: ( j in dom p implies f . (i + j) = p . j )
A13: j in NAT by ORDINAL1:def 12;
assume j in dom p ; :: thesis: f . (i + j) = p . j
then i + j in { (i + k) where k is Element of NAT : k in dom p } by A13;
then ex k being Element of NAT st
( i + j = i + k & f . (i + j) = p . k ) by A6;
hence f . (i + j) = p . j ; :: thesis: verum