reconsider n9 = n as Nat ;

deffunc H_{1}( Nat) -> Element of BOOLEAN = IFEQ (((k div (2 to_power ($1 -' 1))) mod 2),0,FALSE,TRUE);

consider p being FinSequence of BOOLEAN such that

A1: len p = n9 and

A2: for i being Nat st i in dom p holds

p . i = H_{1}(i)
from FINSEQ_2:sch 1();

A3: dom p = Seg n9 by A1, FINSEQ_1:def 3;

reconsider p = p as Element of n -tuples_on BOOLEAN by A1, FINSEQ_2:92;

take p ; :: thesis: for i being Nat st i in Seg n holds

p /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE)

let i be Nat; :: thesis: ( i in Seg n implies p /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) )

assume A4: i in Seg n ; :: thesis: p /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE)

then i in dom p by A1, FINSEQ_1:def 3;

hence p /. i = p . i by PARTFUN1:def 6

.= IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A2, A3, A4 ;

:: thesis: verum

deffunc H

consider p being FinSequence of BOOLEAN such that

A1: len p = n9 and

A2: for i being Nat st i in dom p holds

p . i = H

A3: dom p = Seg n9 by A1, FINSEQ_1:def 3;

reconsider p = p as Element of n -tuples_on BOOLEAN by A1, FINSEQ_2:92;

take p ; :: thesis: for i being Nat st i in Seg n holds

p /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE)

let i be Nat; :: thesis: ( i in Seg n implies p /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) )

assume A4: i in Seg n ; :: thesis: p /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE)

then i in dom p by A1, FINSEQ_1:def 3;

hence p /. i = p . i by PARTFUN1:def 6

.= IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A2, A3, A4 ;

:: thesis: verum