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))*>) )
A1: len (DigitSD x) = n + 1 by CARD_1:def 7;
assume A2: 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))*>)
A3: 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 A4: i in Seg n ; :: thesis: DigA (x,i) = DigA (xn,i)
then i in Seg (n + 1) by FINSEQ_2:8;
then DigA (x,i) = x . i by RADIX_1:def 3
.= xn . i by A2, A4 ;
hence DigA (x,i) = DigA (xn,i) by A4, RADIX_1:def 3; :: thesis: verum

end;

A5: len (DigitSD xn) = n by CARD_1:def 7;
A6: 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 that
A7: 1 <= i and
A8: i <= len (DigitSD x) ; :: thesis: (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i
A9: n + 1 in Seg (n + 1) by FINSEQ_1:3;
i <= n + 1 by A8, CARD_1:def 7;
then A10: i in Seg (n + 1) by A7, FINSEQ_1:1;

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

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

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

then A12: i in Seg (n + 1) by FINSEQ_2:8;
then A13: i in dom (DigitSD x) by A1, FINSEQ_1:def 3;
A14: i in dom (DigitSD xn) by A5, A11, FINSEQ_1:def 3;
then ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i = (DigitSD xn) . i by FINSEQ_1:def 7
.= (DigitSD xn) /. i by A14, PARTFUN1:def 6
.= SubDigit (xn,i,k) by A11, 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 A3, A11
.= ((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 A12, RADIX_1:def 6 ;
hence (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i by A13, PARTFUN1:def 6; :: thesis: verum

end;

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

then A16: i in dom (DigitSD x) by A1, 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 A15, CARD_1:def 7
.= SubDigit (x,(n + 1),k) by FINSEQ_1:42
.= (DigitSD x) /. (n + 1) by A9, RADIX_1:def 6
.= (DigitSD x) . (n + 1) by A15, A16, PARTFUN1:def 6 ;
hence (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i by A15; :: thesis: verum

end;

end;

end;

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

end;

A17: len <*(SubDigit (x,(n + 1),k))*> = 1 by FINSEQ_1:39;
len ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) = (len (DigitSD xn)) + (len <*(SubDigit (x,(n + 1),k))*>) by FINSEQ_1:22
.= n + 1 by A17, CARD_1:def 7 ;
then len (DigitSD x) = len ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) by CARD_1:def 7;
hence Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) by A6, FINSEQ_1:14; :: thesis: verum