:: deftheorem Def1 defines -BinarySequence BINARI_3:def 1 :
for n, k being Nat
for b₃ being Tuple of n, BOOLEAN holds
( b₃ = n -BinarySequence k iff for i being Nat st i in Seg n holds
b₃ /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) );