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 );
A3: 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
A4: ( x = i + k & k in dom p ) ;
[k,(p . k)] in p by A4, FUNCT_1:def 4;
hence ex y being set st S₁[x,y] by A4; :: 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(A3);
{ (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 & k in dom p ) ;
( i + k >= k & k >= 1 & k <= K ) by A1, A7, FINSEQ_1:3, NAT_1:11;
then ( i + k >= 1 & i + k <= i + K ) by XREAL_1:8, XXREAL_0:2;
hence x in Seg (i + K) by A7, FINSEQ_1:3; :: 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 )
A8: j in NAT by ORDINAL1:def 13;
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 A8;
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