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

proof

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

end;