:: deftheorem Def2 defines DigitSD2 RADIX_2:def 2 :
for n, k being Nat
for x, b₄ being Tuple of n, NAT holds
( b₄ = DigitSD2 (x,k) iff for i being Nat st i in Seg n holds
b₄ /. i = SubDigit2 (x,i,k) );