let k, n be Nat; :: thesis: ( n >= 1 implies for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD m,n,k) )
defpred S₁[ Nat] means for m being Nat st m is_represented_by $1,k holds
m = SDDec (DecSD m,$1,k);
A1: S₁[1]

proof

let m be Nat; :: thesis: ( m is_represented_by 1,k implies m = SDDec (DecSD m,1,k) )
assume A2: m is_represented_by 1,k ; :: thesis: m = SDDec (DecSD m,1,k)
A3: 1 in Seg 1 by FINSEQ_1:3;
SubDigit (DecSD m,1,k),1,k = ((Radix k) |^ 0 ) * (DigB (DecSD m,1,k),1) by XREAL_1:234
.= 1 * (DigB (DecSD m,1,k),1) by NEWTON:9
.= m by A2, Th24 ;
then A4: (DigitSD (DecSD m,1,k)) /. 1 = m by A3, Def6;
A5: m is Element of INT by INT_1:def 2;
then reconsider M = <*m*> as FinSequence of INT by FINSEQ_1:95;
thus SDDec (DecSD m,1,k) = Sum M by A4, Th20
.= m by A5, FINSOP_1:12 ; :: thesis: verum

end;

A6: for u being Nat st u >= 1 & S₁[u] holds
S₁[u + 1]

proof

let u be Nat; :: thesis: ( u >= 1 & S₁[u] implies S₁[u + 1] )
assume A7: ( u >= 1 & S₁[u] ) ; :: thesis: S₁[u + 1]
for p being Nat st p is_represented_by u + 1,k holds
p = SDDec (DecSD p,(u + 1),k)

proof

let p be Nat; :: thesis: ( p is_represented_by u + 1,k implies p = SDDec (DecSD p,(u + 1),k) )
assume p is_represented_by u + 1,k ; :: thesis: p = SDDec (DecSD p,(u + 1),k)
then A8: p < (Radix k) |^ (u + 1) by Def12;
set R = (Radix k) |^ u;
Radix k <> 0 by POWER:39;
then (Radix k) |^ u <> 0 by PREPOWER:12;
then A9: (Radix k) |^ u > 0 ;
then A10: p = (((Radix k) |^ u) * (p div ((Radix k) |^ u))) + (p mod ((Radix k) |^ u)) by NAT_D:2;
set M = p mod ((Radix k) |^ u);
set N = ((Radix k) |^ u) * (p div ((Radix k) |^ u));
p mod ((Radix k) |^ u) < (Radix k) |^ u by A9, NAT_D:1;
then p mod ((Radix k) |^ u) is_represented_by u,k by Def12;
then A11: p = (SDDec (DecSD (p mod ((Radix k) |^ u)),u,k)) + (((Radix k) |^ u) * (p div ((Radix k) |^ u))) by A7, A10;
set I = u + 1;
A12: (u + 1) -' 1 = u by NAT_D:34;
then A13: p div ((Radix k) |^ u) = DigitDC p,(u + 1),k by A8, NAT_D:24;
A14: ( 1 <= u + 1 & u + 1 <= u + 1 ) by NAT_1:12;
then A15: u + 1 in Seg (u + 1) by FINSEQ_1:3;
A16: u + 1 <= len (DigitSD (DecSD p,(u + 1),k)) by FINSEQ_1:def 18;
A17: ((Radix k) |^ u) * (p div ((Radix k) |^ u)) = SubDigit (DecSD p,(u + 1),k),(u + 1),k by A12, A13, A15, Def9
.= (DigitSD (DecSD p,(u + 1),k)) /. (u + 1) by A15, Def6
.= (DigitSD (DecSD p,(u + 1),k)) . (u + 1) by A16, FINSEQ_4:24, NAT_1:12 ;
(DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) ^ <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> = DigitSD (DecSD p,(u + 1),k)

proof

A18: ((Radix k) |^ u) * (p div ((Radix k) |^ u)) is Element of INT by INT_1:def 2;
set z0 = DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k);
reconsider z1 = <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> as FinSequence of INT by A18, FINSEQ_1:95;
reconsider DD = DigitSD (DecSD p,(u + 1),k) as FinSequence of INT ;
reconsider z = (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) ^ z1 as FinSequence of INT ;
A19: len z = (len (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k))) + (len <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*>) by FINSEQ_1:35
.= u + (len <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*>) by FINSEQ_1:def 18
.= u + 1 by FINSEQ_1:56 ;
A20: len DD = u + 1 by FINSEQ_1:def 18;
for i being Nat st 1 <= i & i <= len z holds
z /. i = DD /. i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len z implies z /. i = DD /. i )
assume ( 1 <= i & i <= len z ) ; :: thesis: z /. i = DD /. i
then A21: i in Seg (u + 1) by A19, FINSEQ_1:3;

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

suppose A22: i in Seg u ; :: thesis: z /. i = DD /. i

A23: (p mod ((Radix k) |^ u)) mod ((Radix k) |^ i) = p mod ((Radix k) |^ i)

proof

i <= u by A22, FINSEQ_1:3;
then (Radix k) |^ i divides (Radix k) |^ u by Th7;
then consider t being Nat such that
A24: (Radix k) |^ u = ((Radix k) |^ i) * t by NAT_D:def 3;
Radix k <> 0 by POWER:39;
then t <> 0 by A24, PREPOWER:12;
hence (p mod ((Radix k) |^ u)) mod ((Radix k) |^ i) = p mod ((Radix k) |^ i) by A24, Th4; :: thesis: verum

end;

len (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) = u by FINSEQ_1:def 18;
then A25: i in dom (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) by A22, FINSEQ_1:def 3;
then A26: ((DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) ^ z1) . i = (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) . i by FINSEQ_1:def 7
.= (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) /. i by A25, PARTFUN1:def 8
.= SubDigit (DecSD (p mod ((Radix k) |^ u)),u,k),i,k by A22, Def6
.= ((Radix k) |^ (i -' 1)) * (DigitDC (p mod ((Radix k) |^ u)),i,k) by A22, Def9
.= ((Radix k) |^ (i -' 1)) * ((p mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1))) by A23 ;
len DD = u + 1 by FINSEQ_1:def 18;
then A27: i in dom DD by A21, FINSEQ_1:def 3;
then A28: DD . i = (DigitSD (DecSD p,(u + 1),k)) /. i by PARTFUN1:def 8
.= SubDigit (DecSD p,(u + 1),k),i,k by A21, Def6
.= ((Radix k) |^ (i -' 1)) * (DigitDC p,i,k) by A21, Def9
.= ((Radix k) |^ (i -' 1)) * ((p mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1))) ;
A29: DD . i = DD /. i by A27, PARTFUN1:def 8;
i in dom ((DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) ^ z1) by A19, A21, FINSEQ_1:def 3;
hence z /. i = DD /. i by A26, A28, A29, PARTFUN1:def 8; :: thesis: verum

end;

suppose A30: i = u + 1 ; :: thesis: z /. i = DD /. i

hence z /. i = z . (u + 1) by A14, A19, FINSEQ_4:24
.= ((DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) ^ z1) . ((len (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k))) + 1) by FINSEQ_1:def 18
.= (DigitSD (DecSD p,(u + 1),k)) . (u + 1) by A17, FINSEQ_1:59
.= DD /. i by A16, A30, FINSEQ_4:24, NAT_1:12 ;
:: thesis: verum

end;

end;

end;

hence (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) ^ <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> = DigitSD (DecSD p,(u + 1),k) by A19, A20, FINSEQ_5:14; :: thesis: verum

end;

hence p = SDDec (DecSD p,(u + 1),k) by A11, RVSUM_1:104; :: thesis: verum

end;

hence S₁[u + 1] ; :: thesis: verum

end;

for u being Nat st u >= 1 holds
S₁[u] from NAT_1:sch 8(A1, A6);
hence ( n >= 1 implies for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD m,n,k) ) ; :: thesis: verum