let k, n be Nat; for x being Tuple of n + 1,k -SD
for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
x . i = xn . i ) holds
(SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x
let x be Tuple of n + 1,k -SD ; for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
x . i = xn . i ) holds
(SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x
let xn be Tuple of n,k -SD ; ( ( for i being Nat st i in Seg n holds
x . i = xn . i ) implies (SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x )
assume A1:
for i being Nat st i in Seg n holds
x . i = xn . i
; (SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x
SDDec x =
Sum (DigitSD x)
by RADIX_1:def 7
.=
Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>)
by A1, Th9
.=
(Sum (DigitSD xn)) + (SubDigit (x,(n + 1),k))
by RVSUM_1:74
.=
(Sum (DigitSD xn)) + (((Radix k) |^ ((n + 1) -' 1)) * (DigB (x,(n + 1))))
by RADIX_1:def 5
.=
(Sum (DigitSD xn)) + (((Radix k) |^ n) * (DigB (x,(n + 1))))
by NAT_D:34
.=
(Sum (DigitSD xn)) + (((Radix k) |^ n) * (DigA (x,(n + 1))))
by RADIX_1:def 4
;
hence
(SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x
by RADIX_1:def 7; verum