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