let p1, p2 be Tuple of n, BOOLEAN ; ( ( 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)
; 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 for i being Nat st i in dom p1 holds
p1 . i = p2 . ilet i be
Nat;
( i in dom p1 implies p1 . i = p2 . i )assume A10:
i in dom p1
;
p1 . i = p2 . ithen 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
;
verum end;
hence
p1 = p2
by A7, A9, FINSEQ_2:9; verum