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:1;
now :: thesis: SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0
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