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:3;
then A3:
n + 1 in Seg ((n + 1) + 1)
by FINSEQ_2:8;
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:6
;
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