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 ;
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 ;
hence (SDSub_Add_Data ((DigA (a,i)),k)) + (SDSub_Add_Carry ((DigA (a,(i -' 1))),k)) in k -SD_Sub by ; :: thesis: verum
end;
hence SD2SDSubDigit (a,i,k) in k -SD_Sub by ; :: 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 ;
then SDSub_Add_Carry ((DigA (a,(i -' 1))),k) in k -SD_Sub ;
hence SD2SDSubDigit (a,i,k) in k -SD_Sub by ; :: thesis: verum
end;
end;
end;
hence SD2SDSubDigit (a,i,k) is Element of k -SD_Sub ; :: thesis: verum