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;
end;
end;
hence SD2SDSubDigit (a,i,k) is Element of k -SD_Sub ; :: thesis: verum