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