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:3;
then A2: i <= n + 1 by NAT_1:12;
A3: 1 <= i by A1, FINSEQ_1:3;
then A4: i in Seg (n + 1) by A2, FINSEQ_1:3;
i <= (n + 1) + 1 by A2, NAT_1:12;
then A5: i in Seg ((n + 1) + 1) by A3, FINSEQ_1:3;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
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

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:234
.= 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:234
.= 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:234
.= 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:234
.= 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:21;
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:3;
then 1 < i by A13, XXREAL_0:1;
then A14: 0 + 1 <= i -' 1 by INT_1:20, JORDAN12:1;
i <= n by A1, FINSEQ_1:3;
then i -' 1 <= n by NAT_D:44;
then A15: i -' 1 in Seg n by A14, FINSEQ_1:3;
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:21
.= (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:21
.= (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:21
.= (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:21
.= 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