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 A1: ( 2 <= k & i in Seg (n + 1) ) ; :: thesis: SD2SDSubDigit a,i,k is Element of k -SD_Sub
set SDC = SDSub_Add_Carry (DigA a,(i -' 1)),k;
set SDD = (SDSub_Add_Data (DigA a,i),k) + (SDSub_Add_Carry (DigA a,(i -' 1)),k);
A2: ( 1 <= i & i <= n + 1 ) by A1, FINSEQ_1:3;
then A3: i -' 1 = i - 1 by XREAL_1:235;

now

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

suppose A4: 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

A5: DigA a,i is Element of k -SD by A4, RADIX_1:19;
A6: ( 1 <= i & i <= n ) by A4, FINSEQ_1:3;

now

per cases ( i = 1 or i > 1 ) by A6, XXREAL_0:1;

suppose i = 1 ; :: thesis: (SDSub_Add_Data (DigA a,i),k) + (SDSub_Add_Carry (DigA a,(i -' 1)),k) in k -SD_Sub

then i -' 1 = 0 by NAT_2:10;
then DigA a,(i -' 1) = 0 by RADIX_1:def 3;
then DigA a,(i -' 1) in k -SD by 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, A5, Th16; :: thesis: verum

end;

suppose i > 1 ; :: thesis: (SDSub_Add_Data (DigA a,i),k) + (SDSub_Add_Carry (DigA a,(i -' 1)),k) in k -SD_Sub

then A7: i -' 1 >= 1 by NAT_D:49;
i - 1 <= n by A2, XREAL_1:22;
then i -' 1 in Seg n by A3, A7, FINSEQ_1:3;
then DigA a,(i -' 1) is Element of k -SD by 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, A5, Th16; :: thesis: verum

end;

end;

end;

hence (SDSub_Add_Data (DigA a,i),k) + (SDSub_Add_Carry (DigA a,(i -' 1)),k) in k -SD_Sub ; :: thesis: verum

end;

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

end;

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

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

proof

A9: SDSub_Add_Carry (DigA a,(i -' 1)),k in k -SD_Sub_S by A1, Th15;
k -SD_Sub_S c= k -SD_Sub by Th3;
hence SDSub_Add_Carry (DigA a,(i -' 1)),k in k -SD_Sub by A9; :: thesis: verum

end;

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

end;

end;

end;

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