:: deftheorem Def2 defines '+' RADIX_4:def 2 :
for n, k being Nat
for x, y, b₅ being Tuple of n,k -SD_Sub holds
( b₅ = x '+' y iff for i being Nat st i in Seg n holds
DigA_SDSub (b₅,i) = SDSubAddDigit (x,y,i,k) );