deffunc H₁( Nat) -> set = p . ((len p) - ($1 + 1));
ex q being XFinSequence st
( len q = len p & ( for k being Nat st k in len p holds
q . k = H₁(k) ) ) from AFINSQ_1:sch 2();
hence ex b₁ being XFinSequence st
( len b₁ = len p & ( for i being Nat st i in dom b₁ holds
b₁ . i = p . ((len p) - (i + 1)) ) ) ; :: thesis: verum