let n, k, x, y, i be Nat; :: thesis: ( i in Seg n & 2 <= k implies SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) )
set X = x mod ((Radix k) |^ n);
set Y = y mod ((Radix k) |^ n);
assume A1: i in Seg n ; :: thesis: ( not 2 <= k or SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) )
then i <= n by FINSEQ_1:1;
then A2: i <= n + 1 by NAT_1:12;
A3: 1 <= i by A1, FINSEQ_1:1;
then A4: i in Seg (n + 1) by A2, FINSEQ_1:1;
i <= (n + 1) + 1 by A2, NAT_1:12;
then A5: i in Seg ((n + 1) + 1) by A3, FINSEQ_1:1;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
assume A6: 2 <= k ; :: thesis: SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)
then A7: SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k)) by A5, Def1;

now :: thesis: SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)

per cases ( i = 1 or i <> 1 ) ;

suppose A8: i = 1 ; :: thesis: SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)

then A9: DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(i -' 1)) = DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),0) by XREAL_1:232
.= 0 by RADIX_3:def 5 ;
A10: DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(i -' 1)) = DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),0) by A8, XREAL_1:232
.= 0 by RADIX_3:def 5 ;
A11: DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)) = DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),0) by A8, XREAL_1:232
.= 0 by RADIX_3:def 5 ;
A12: DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1)) = DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),0) by A8, XREAL_1:232
.= 0 by RADIX_3:def 5 ;
( DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i) & DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i) ) by A1, A6, RADIX_3:20;
hence SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) by A4, A6, A7, A12, A11, A10, A9, Def1; :: thesis: verum

end;

suppose A13: i <> 1 ; :: thesis: SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)

i >= 1 by A1, FINSEQ_1:1;
then 1 < i by A13, XXREAL_0:1;
then A14: 0 + 1 <= i -' 1 by INT_1:7, JORDAN12:1;
i <= n by A1, FINSEQ_1:1;
then i -' 1 <= n by NAT_D:44;
then A15: i -' 1 in Seg n by A14, FINSEQ_1:1;
SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k)) by A1, A6, A7, RADIX_3:20
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k)) by A1, A6, RADIX_3:20
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k)) by A6, A15, RADIX_3:20
.= (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(i -' 1)))),k)) by A6, A15, RADIX_3:20
.= SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) by A4, A6, Def1 ;
hence SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) ; :: thesis: verum

end;

end;

end;

hence SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) ; :: thesis: verum