let k, m, n be Nat; :: thesis:
assume that
A1: k >= 2 and
A2: m is_represented_by 1,k and
A3: n is_represented_by 1,k ; :: thesis:
set N = DecSD n,1,k;
set M = DecSD m,1,k;
A4: 1 in Seg 1 by FINSEQ_1:3;
then A5: DigA ((DecSD m,1,k) '+' (DecSD n,1,k)),1 = Add (DecSD m,1,k),(DecSD n,1,k),1,k by Def14
.= (SD_Add_Data ((DigA (DecSD m,1,k),1) + (DigA (DecSD n,1,k),1)),k) + (SD_Add_Carry ((DigA (DecSD m,1,k),(1 -' 1)) + (DigA (DecSD n,1,k),(1 -' 1)))) by A1, A4, Def13
.= (SD_Add_Data ((DigA (DecSD m,1,k),1) + (DigA (DecSD n,1,k),1)),k) + (SD_Add_Carry ((DigA (DecSD m,1,k),0 ) + (DigA (DecSD n,1,k),(1 -' 1)))) by XREAL_1:234
.= (SD_Add_Data ((DigA (DecSD m,1,k),1) + (DigA (DecSD n,1,k),1)),k) + (SD_Add_Carry ((DigA (DecSD m,1,k),0 ) + (DigA (DecSD n,1,k),0 ))) by XREAL_1:234
.= (SD_Add_Data ((DigA (DecSD m,1,k),1) + (DigA (DecSD n,1,k),1)),k) + (SD_Add_Carry (0 + (DigA (DecSD n,1,k),0 ))) by Def3
.= (SD_Add_Data ((DigA (DecSD m,1,k),1) + (DigA (DecSD n,1,k),1)),k) + 0 by Def3, Th21
.= SD_Add_Data (m + (DigA (DecSD n,1,k),1)),k by A2, Th24
.= SD_Add_Data (m + n),k by A3, Th24 ;
A6: (DigitSD ((DecSD m,1,k) '+' (DecSD n,1,k))) /. 1 = SubDigit ((DecSD m,1,k) '+' (DecSD n,1,k)),1,k by A4, Def6
.= ((Radix k) |^ 0 ) * (DigA ((DecSD m,1,k) '+' (DecSD n,1,k)),1) by XREAL_1:234
.= 1 * (DigA ((DecSD m,1,k) '+' (DecSD n,1,k)),1) by NEWTON:9
.= SD_Add_Data (m + n),k by A5 ;
reconsider w = SD_Add_Data (m + n),k as Element of INT by INT_1:def 2;
A7: len (DigitSD ((DecSD m,1,k) '+' (DecSD n,1,k))) = 1 by FINSEQ_1:def 18;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom (DigitSD ((DecSD m,1,k) '+' (DecSD n,1,k))) by A7, FINSEQ_1:def 3;
then (DigitSD ((DecSD m,1,k) '+' (DecSD n,1,k))) . 1 = SD_Add_Data (m + n),k by A6, PARTFUN1:def 8;
then SDDec ((DecSD m,1,k) '+' (DecSD n,1,k)) = Sum <*w*> by A7, FINSEQ_1:57
.= SD_Add_Data (m + n),k by RVSUM_1:103 ;
hence SDDec ((DecSD m,1,k) '+' (DecSD n,1,k)) = SD_Add_Data (m + n),k ; :: thesis: