:: deftheorem Def1 defines Bin1 BINARI_2:def 1 :
for n being Nat
for b₂ being Tuple of n, BOOLEAN holds
( b₂ = Bin1 n iff for i being Nat st i in Seg n holds
b₂ /. i = IFEQ (i,1,TRUE,FALSE) );