let i, n, k be Nat; :: thesis: for a being Tuple of n,k -SD st 2 <= k & i in Seg (n + 1) holds
SD2SDSubDigit (a,i,k) is Element of k -SD_Sub
let a be Tuple of n,k -SD ; :: thesis: ( 2 <= k & i in Seg (n + 1) implies SD2SDSubDigit (a,i,k) is Element of k -SD_Sub )
assume that
A1: 2 <= k and
A2: i in Seg (n + 1) ; :: thesis: SD2SDSubDigit (a,i,k) is Element of k -SD_Sub
set SDD = (SDSub_Add_Data ((DigA (a,i)),k)) + (SDSub_Add_Carry ((DigA (a,(i -' 1))),k));
set SDC = SDSub_Add_Carry ((DigA (a,(i -' 1))),k);

now :: thesis: SD2SDSubDigit (a,i,k) in k -SD_Sub

per cases ( i in Seg n or i = n + 1 ) by A2, FINSEQ_2:7;

suppose A3: i in Seg n ; :: thesis: SD2SDSubDigit (a,i,k) in k -SD_Sub

(SDSub_Add_Data ((DigA (a,i)),k)) + (SDSub_Add_Carry ((DigA (a,(i -' 1))),k)) in k -SD_Sub

proof

DigA (a,i) is Element of k -SD by A3, RADIX_1:16;
hence (SDSub_Add_Data ((DigA (a,i)),k)) + (SDSub_Add_Carry ((DigA (a,(i -' 1))),k)) in k -SD_Sub by A1, Th15; :: thesis: verum

end;

hence SD2SDSubDigit (a,i,k) in k -SD_Sub by A3, Def6; :: thesis: verum

end;

suppose A4: i = n + 1 ; :: thesis: SD2SDSubDigit (a,i,k) in k -SD_Sub

( SDSub_Add_Carry ((DigA (a,(i -' 1))),k) in k -SD_Sub_S & k -SD_Sub_S c= k -SD_Sub ) by A1, Th2, Th14;
then SDSub_Add_Carry ((DigA (a,(i -' 1))),k) in k -SD_Sub ;
hence SD2SDSubDigit (a,i,k) in k -SD_Sub by A4, Def6; :: thesis: verum

end;

end;

end;

hence SD2SDSubDigit (a,i,k) is Element of k -SD_Sub ; :: thesis: verum