deffunc H₁( 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₁(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