deffunc H_{1}( Nat) -> set = ($1 - 1) / (2 |^ n);

consider FS being FinSequence such that

A1: ( len FS = (2 |^ n) + 1 & ( for i being Nat st i in dom FS holds

FS . i = H_{1}(i) ) )
from FINSEQ_1:sch 2();

take FS ; :: thesis: ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom FS holds

FS . i = (i - 1) / (2 |^ n) ) )

thus ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom FS holds

FS . i = (i - 1) / (2 |^ n) ) ) by A1, FINSEQ_1:def 3; :: thesis: verum

consider FS being FinSequence such that

A1: ( len FS = (2 |^ n) + 1 & ( for i being Nat st i in dom FS holds

FS . i = H

take FS ; :: thesis: ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom FS holds

FS . i = (i - 1) / (2 |^ n) ) )

thus ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom FS holds

FS . i = (i - 1) / (2 |^ n) ) ) by A1, FINSEQ_1:def 3; :: thesis: verum