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
Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>)
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
Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>)
let xn be Tuple of n,(k -SD ); :: thesis: ( ( for i being Nat st i in Seg n holds
x . i = xn . i ) implies Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) )
assume A1: for i being Nat st i in Seg n holds
x . i = xn . i ; :: thesis: Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>)
A2: len (DigitSD x) = n + 1 by FINSEQ_1:def 18;
A3: len (DigitSD xn) = n by FINSEQ_1:def 18;
A4: len <*(SubDigit x,(n + 1),k)*> = 1 by FINSEQ_1:56;
len ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) = (len (DigitSD xn)) + (len <*(SubDigit x,(n + 1),k)*>) by FINSEQ_1:35
.= n + 1 by A4, FINSEQ_1:def 18 ;
then A5: len (DigitSD x) = len ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) by FINSEQ_1:def 18;
A6: for i being Element of NAT st i in Seg n holds
DigA x,i = DigA xn,i

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies DigA x,i = DigA xn,i )
assume A7: i in Seg n ; :: thesis: DigA x,i = DigA xn,i
then i in Seg (n + 1) by FINSEQ_2:9;
then DigA x,i = x . i by RADIX_1:def 3
.= xn . i by A1, A7 ;
hence DigA x,i = DigA xn,i by A7, RADIX_1:def 3; :: thesis: verum

end;

for i being Nat st 1 <= i & i <= len (DigitSD x) holds
(DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (DigitSD x) implies (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i )
assume ( 1 <= i & i <= len (DigitSD x) ) ; :: thesis: (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i
then ( 1 <= i & i <= n + 1 ) by FINSEQ_1:def 18;
then A8: i in Seg (n + 1) by FINSEQ_1:3;
A9: n + 1 in Seg (n + 1) by FINSEQ_1:5;

now

per cases ( i in Seg n or i = n + 1 ) by A8, FINSEQ_2:8;

suppose A10: i in Seg n ; :: thesis: (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i

then A11: i in Seg (n + 1) by FINSEQ_2:9;
A12: i in dom (DigitSD xn) by A3, A10, FINSEQ_1:def 3;
A13: i in dom (DigitSD x) by A2, A11, FINSEQ_1:def 3;
((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i = (DigitSD xn) . i by A12, FINSEQ_1:def 7
.= (DigitSD xn) /. i by A12, PARTFUN1:def 8
.= SubDigit xn,i,k by A10, RADIX_1:def 6
.= ((Radix k) |^ (i -' 1)) * (DigB xn,i) by RADIX_1:def 5
.= ((Radix k) |^ (i -' 1)) * (DigA xn,i) by RADIX_1:def 4
.= ((Radix k) |^ (i -' 1)) * (DigA x,i) by A6, A10
.= ((Radix k) |^ (i -' 1)) * (DigB x,i) by RADIX_1:def 4
.= SubDigit x,i,k by RADIX_1:def 5
.= (DigitSD x) /. i by A11, RADIX_1:def 6 ;
hence (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i by A13, PARTFUN1:def 8; :: thesis: verum

end;

suppose A14: i = n + 1 ; :: thesis: (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i

then A15: i in dom (DigitSD x) by A2, A9, FINSEQ_1:def 3;
((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i = ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . ((len (DigitSD xn)) + 1) by A14, FINSEQ_1:def 18
.= SubDigit x,(n + 1),k by FINSEQ_1:59
.= (DigitSD x) /. (n + 1) by A9, RADIX_1:def 6
.= (DigitSD x) . (n + 1) by A14, A15, PARTFUN1:def 8 ;
hence (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i by A14; :: thesis: verum

end;

end;

end;

hence (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) . i ; :: thesis: verum

end;

hence Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) by A5, FINSEQ_1:18; :: thesis: verum