deffunc H₁( Nat) -> Element of NAT = IFEQ (x /. $1),FALSE ,0 ,(2 to_power ($1 -' 1));
consider z being FinSequence of NAT such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H₁(j) from FINSEQ_2:sch 1();
A3: dom z = Seg n by A1, FINSEQ_1:def 3;
reconsider z = z as Tuple of n,NAT by A1, FINSEQ_2:110;
take z ; :: thesis: for i being Nat st i in Seg n holds
z /. i = IFEQ (x /. i),FALSE ,0 ,(2 to_power (i -' 1))
let j be Nat; :: thesis: ( j in Seg n implies z /. j = IFEQ (x /. j),FALSE ,0 ,(2 to_power (j -' 1)) )
assume A4: j in Seg n ; :: thesis: z /. j = IFEQ (x /. j),FALSE ,0 ,(2 to_power (j -' 1))
then j in dom z by A1, FINSEQ_1:def 3;
hence z /. j = z . j by PARTFUN1:def 8
.= IFEQ (x /. j),FALSE ,0 ,(2 to_power (j -' 1)) by A2, A4, A3 ;
:: thesis: verum