deffunc H_{1}( 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_{1}(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, CARD_1:def 7;

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 6

.= IFEQ ((x /. j),FALSE,0,(2 to_power (j -' 1))) by A2, A3, A4 ;

:: thesis: verum

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

A3: dom z = Seg n by A1, FINSEQ_1:def 3;

reconsider z = z as Tuple of n, NAT by A1, CARD_1:def 7;

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 6

.= IFEQ ((x /. j),FALSE,0,(2 to_power (j -' 1))) by A2, A3, A4 ;

:: thesis: verum