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 & len p2 = n ) by FINSEQ_1:def 18;
X: dom p1 = Seg n by A7, FINSEQ_1:def 3;

now

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

end;

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