deffunc H₁( Nat) -> set = p . ($1 + (x .. p));
reconsider n = (len p) - (x .. p) as Element of NAT by A1, Th22;
consider q being FinSequence such that
A2: ( len q = n & ( for k being Nat st k in dom q holds
q . k = H₁(k) ) ) from FINSEQ_1:sch 2();
take q ; :: thesis: ( len q = (len p) - (x .. p) & ( for k being Nat st k in dom q holds
q . k = p . (k + (x .. p)) ) )
thus ( len q = (len p) - (x .. p) & ( for k being Nat st k in dom q holds
q . k = p . (k + (x .. p)) ) ) by A2; :: thesis: verum