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:104
.= (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