deffunc H₁( Nat) -> set = q . ($1 - 1);
ex p being FinSequence st
( len p = len q & ( for k being Nat st k in dom p holds
p . k = H₁(k) ) ) from FINSEQ_1:sch 2();
then consider p being FinSequence such that
A1: len p = len q and
A2: for k being Nat st k in dom p holds
p . k = H₁(k) ;
A11: dom p = Seg (len q) by A1, FINSEQ_1:def 3;
for i being Nat st 1 <= i & i <= len q holds
q . (i - 1) = p . i by A2, A11, FINSEQ_1:1;
hence ex b₁ being FinSequence st
( len b₁ = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i - 1) = b₁ . i ) ) by A1; :: thesis: verum