:: deftheorem Def3 defines Binary BINARITH:def 3 :
for n being Nat
for x being Tuple of n, BOOLEAN
for b₃ being Tuple of n, NAT holds
( b₃ = Binary x iff for i being Nat st i in Seg n holds
b₃ /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) );