let k, i, n 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

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

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:19;
hence (SDSub_Add_Data (DigA a,i),k) + (SDSub_Add_Carry (DigA a,(i -' 1)),k) in k -SD_Sub by A1, Th16; :: thesis: verum

end;

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

end;

suppose A6: 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, Th3, Th15;
then SDSub_Add_Carry (DigA a,(i -' 1)),k in k -SD_Sub ;
hence SD2SDSubDigit a,i,k in k -SD_Sub by A6, Def6; :: thesis: verum

end;

end;

end;

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