let k, m, n be Nat; ( k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k implies SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k) )
assume that
A1:
k >= 2
and
A2:
m is_represented_by 1,k
and
A3:
n is_represented_by 1,k
; SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k)
set N = DecSD (n,1,k);
set M = DecSD (m,1,k);
A4:
1 in Seg 1
by FINSEQ_1:1;
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:232
.=
(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:232
.=
(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, Th17
.=
SD_Add_Data ((m + (DigA ((DecSD (n,1,k)),1))),k)
by A2, Th20
.=
SD_Add_Data ((m + n),k)
by A3, Th20
;
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:232
.=
1 * (DigA (((DecSD (m,1,k)) '+' (DecSD (n,1,k))),1))
by NEWTON:4
.=
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 CARD_1:def 7;
1 in Seg 1
by FINSEQ_1:1;
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 6;
then SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) =
Sum <*w*>
by A7, FINSEQ_1:40
.=
SD_Add_Data ((m + n),k)
by RVSUM_1:73
;
hence
SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k)
; verum