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;

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

hence
p1 = p2
by A7, A9, FINSEQ_2:9; :: thesis: verump1 . 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;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