let n, k, i be Nat; :: thesis: ( 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 ; :: thesis: SD_Add_Carry (DigA (DecSD 1,n,k),i) = 0
A3: i >= 1 by A2, FINSEQ_1:3;

now

per cases ( i = 1 or i > 1 ) by A3, XXREAL_0:1;

suppose i = 1 ; :: thesis: SD_Add_Carry (DigA (DecSD 1,n,k),i) = 0

then SD_Add_Carry (DigA (DecSD 1,n,k),i) = SD_Add_Carry 1 by A1, A2, Th7;
hence SD_Add_Carry (DigA (DecSD 1,n,k),i) = 0 by RADIX_1:def 10; :: thesis: verum

end;

suppose i > 1 ; :: thesis: SD_Add_Carry (DigA (DecSD 1,n,k),i) = 0

then SD_Add_Carry (DigA (DecSD 1,n,k),i) = SD_Add_Carry 0 by A1, A2, Th8;
hence SD_Add_Carry (DigA (DecSD 1,n,k),i) = 0 by RADIX_1:def 10; :: thesis: verum

end;

end;

end;

hence SD_Add_Carry (DigA (DecSD 1,n,k),i) = 0 ; :: thesis: verum