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

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