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 FINSEQ_1:def 18;
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:9;
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 FINSEQ_1:def 18;
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:5;
i <= n + 1 by A8, FINSEQ_1:def 18;
then A10: i in Seg (n + 1) by A7, FINSEQ_1:3;

now

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

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:9;
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 8
.= 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 8; :: 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, 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 A15, A16, PARTFUN1:def 8 ;
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: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 A17, FINSEQ_1:def 18 ;
then len (DigitSD x) = len ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) by FINSEQ_1:def 18;
hence Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit x,(n + 1),k)*>) by A6, FINSEQ_1:18; :: thesis: verum