let n be Element of NAT ; :: thesis: ex FS being FinSequence st
( dom FS = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom FS holds
FS . i = (i - 1) / (2 |^ n) ) )
deffunc H₁( Nat) -> Element of REAL = ($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();
A2: dom FS = Seg ((2 |^ n) + 1) by A1, FINSEQ_1:def 3;
take FS ; :: thesis: ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom FS holds
FS . i = (i - 1) / (2 |^ n) ) )
thus ( dom FS = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom FS holds
FS . i = (i - 1) / (2 |^ n) ) ) by A1, A2; :: thesis: verum