let n, k, i be Nat; ( k >= 2 & i in Seg n implies SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0 )
assume that
A1:
k >= 2
and
A2:
i in Seg n
; SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0
A3:
i >= 1
by A2, FINSEQ_1:1;
hence
SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0
; verum