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 CARD_1:def 7;
then A8: dom p1 = Seg n by FINSEQ_1:def 3;
A9: len p2 = n by CARD_1:def 7;

now :: thesis: for i being Nat st i in dom p1 holds
p1 . i = p2 . i

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 6
.= 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 6 ; :: thesis: verum

end;

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