thus ex p1 being XFinSequence st
( len p1 = (len p) -' n & ( for m being Nat st m in dom p1 holds
p1 . m = p . (m + n) ) ) :: thesis:

deffunc H₁( Nat) -> set = p . ($1 + n);
set k = (len p) -' n;
consider q being XFinSequence such that
A1: ( len q = (len p) -' n & ( for m2 being Nat st m2 in (len p) -' n holds
q . m2 = H₁(m2) ) ) from AFINSQ_1:sch 2();
take q ; :: thesis:
thus ( len q = (len p) -' n & ( for m being Nat st m in dom q holds
q . m = p . (m + n) ) ) by A1; :: thesis:

end;