let p1, p2 be Tuple of n, BOOLEAN ; :: thesis: ( ( for i being Nat st i in Seg n holds
p1 /. i = IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE ) & ( for i being Nat st i in Seg n holds
p2 /. i = IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE ) implies p1 = p2 )
assume that
A5: for i being Nat st i in Seg n holds
p1 /. i = IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE and
A6: for i being Nat st i in Seg n holds
p2 /. i = IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE ; :: thesis: p1 = p2
A7: len p1 = n by FINSEQ_1:def 18;
then A8: dom p1 = Seg n by FINSEQ_1:def 3;
A9: len p2 = n by FINSEQ_1:def 18;

now

let i be Nat; :: thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume A10: i in dom p1 ; :: thesis: p1 . i = p2 . i
then A11: i in dom p2 by A9, A8, FINSEQ_1:def 3;
thus p1 . i = p1 /. i by A10, PARTFUN1:def 8
.= IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE by A5, A8, A10
.= p2 /. i by A6, A8, A10
.= p2 . i by A11, PARTFUN1:def 8 ; :: thesis: verum

end;

hence p1 = p2 by A7, A9, FINSEQ_2:10; :: thesis: verum