reconsider n9 = n as Nat ;
deffunc H₁( 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₁(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:110;
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 8
.= IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE by A2, A3, A4 ;
:: thesis: verum