let z1, z2 be Tuple of n, NAT ; :: thesis: ( ( for i being Nat st i in Seg n holds
z1 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) & ( for i being Nat st i in Seg n holds
z2 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) implies z1 = z2 )
assume that
A5: for i being Nat st i in Seg n holds
z1 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) and
A6: for i being Nat st i in Seg n holds
z2 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ; :: thesis: z1 = z2
A7: len z1 = n by CARD_1:def 7;
then A8: dom z1 = Seg n by FINSEQ_1:def 3;
A9: len z2 = n by CARD_1:def 7;
then A10: dom z2 = Seg n by FINSEQ_1:def 3;

now :: thesis: for j being Nat st j in dom z1 holds
z1 . j = z2 . j

let j be Nat; :: thesis: ( j in dom z1 implies z1 . j = z2 . j )
assume A11: j in dom z1 ; :: thesis: z1 . j = z2 . j
hence z1 . j = z1 /. j by PARTFUN1:def 6
.= IFEQ ((x /. j),FALSE,0,(2 to_power (j -' 1))) by A5, A8, A11
.= z2 /. j by A6, A8, A11
.= z2 . j by A8, A10, A11, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence z1 = z2 by A7, A9, FINSEQ_2:9; :: thesis: verum