let k, n be Nat; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( ( 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 ; :: thesis: (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; :: thesis: verum