let k, x, n be Nat; ( k >= 2 implies ((Radix k) |^ n) * (DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) = ((((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(n + 1)),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),n),k)) )
assume A1:
k >= 2
; ((Radix k) |^ n) * (DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) = ((((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(n + 1)),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),n),k))
A2:
n + 1 in Seg (n + 1)
by FINSEQ_1:5;
then A3:
n + 1 in Seg ((n + 1) + 1)
by FINSEQ_2:9;
then ((Radix k) |^ n) * (DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) =
((Radix k) |^ n) * (SD2SDSubDigitS (DecSD x,(n + 1),k),(n + 1),k)
by RADIX_3:def 8
.=
((Radix k) |^ n) * (SD2SDSubDigit (DecSD x,(n + 1),k),(n + 1),k)
by A1, A3, RADIX_3:def 7
.=
((Radix k) |^ n) * ((SDSub_Add_Data (DigA (DecSD x,(n + 1),k),(n + 1)),k) + (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),((n + 1) -' 1)),k))
by A2, RADIX_3:def 6
.=
((Radix k) |^ n) * ((SDSub_Add_Data (DigA (DecSD x,(n + 1),k),(n + 1)),k) + (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),n),k))
by NAT_D:34
.=
((Radix k) |^ n) * (((DigA (DecSD x,(n + 1),k),(n + 1)) - ((Radix k) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(n + 1)),k))) + (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),n),k))
by RADIX_3:def 4
.=
((((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1))) - ((((Radix k) |^ n) * (Radix k)) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(n + 1)),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),n),k))
.=
((((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(n + 1)),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),n),k))
by NEWTON:11
;
hence
((Radix k) |^ n) * (DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) = ((((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(n + 1)),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),n),k))
; verum