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: 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 that
u >= 1 and
A2: 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) )
set I = u + 1;
set R = (Radix k) |^ u;
set M = p mod ((Radix k) |^ u);
set N = ((Radix k) |^ u) * (p div ((Radix k) |^ u));
A3: (u + 1) -' 1 = u by NAT_D:34;
A4: u + 1 <= len (DigitSD (DecSD p,(u + 1),k)) by FINSEQ_1:def 18;
A5: 1 <= u + 1 by NAT_1:12;
then A6: u + 1 in Seg (u + 1) by FINSEQ_1:3;
assume p is_represented_by u + 1,k ; :: thesis: p = SDDec (DecSD p,(u + 1),k)
then p < (Radix k) |^ (u + 1) by Def12;
then p div ((Radix k) |^ u) = DigitDC p,(u + 1),k by A3, NAT_D:24;
then A7: ((Radix k) |^ u) * (p div ((Radix k) |^ u)) = SubDigit (DecSD p,(u + 1),k),(u + 1),k by A3, A6, Def9
.= (DigitSD (DecSD p,(u + 1),k)) /. (u + 1) by A6, Def6
.= (DigitSD (DecSD p,(u + 1),k)) . (u + 1) by A4, FINSEQ_4:24, NAT_1:12 ;
A8: (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) ^ <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> = DigitSD (DecSD p,(u + 1),k)

proof

((Radix k) |^ u) * (p div ((Radix k) |^ u)) is Element of INT by INT_1:def 2;
then reconsider z1 = <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> as FinSequence of INT by FINSEQ_1:95;
reconsider DD = DigitSD (DecSD p,(u + 1),k) as FinSequence of INT ;
set z0 = DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k);
reconsider z = (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) ^ z1 as FinSequence of INT ;
A9: 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 ;
A10: 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 A11: i in Seg (u + 1) by A9, FINSEQ_1:3;

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

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

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

proof

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

end;

A15: i in dom ((DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) ^ z1) by A9, A11, FINSEQ_1:def 3;
len DD = u + 1 by FINSEQ_1:def 18;
then A16: i in dom DD by A11, FINSEQ_1:def 3;
then A17: DD . i = DD /. i by PARTFUN1:def 8;
A18: DD . i = (DigitSD (DecSD p,(u + 1),k)) /. i by A16, PARTFUN1:def 8
.= SubDigit (DecSD p,(u + 1),k),i,k by A11, Def6
.= ((Radix k) |^ (i -' 1)) * (DigitDC p,i,k) by A11, Def9
.= ((Radix k) |^ (i -' 1)) * ((p mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1))) ;
len (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) = u by FINSEQ_1:def 18;
then A19: i in dom (DigitSD (DecSD (p mod ((Radix k) |^ u)),u,k)) by A12, FINSEQ_1:def 3;
then ((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 A19, PARTFUN1:def 8
.= SubDigit (DecSD (p mod ((Radix k) |^ u)),u,k),i,k by A12, Def6
.= ((Radix k) |^ (i -' 1)) * (DigitDC (p mod ((Radix k) |^ u)),i,k) by A12, Def9
.= ((Radix k) |^ (i -' 1)) * ((p mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1))) by A13 ;
hence z /. i = DD /. i by A18, A17, A15, PARTFUN1:def 8; :: thesis: verum

end;

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

hence z /. i = z . (u + 1) by A5, A9, 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 A7, FINSEQ_1:59
.= DD /. i by A4, A20, FINSEQ_4:24, NAT_1:12 ;
:: thesis: verum

end;

end;

end;

len DD = u + 1 by FINSEQ_1:def 18;
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 A9, A10, FINSEQ_5:14; :: thesis: verum

end;

Radix k <> 0 by POWER:39;
then A21: (Radix k) |^ u <> 0 by PREPOWER:12;
then p mod ((Radix k) |^ u) < (Radix k) |^ u by NAT_D:1;
then A22: p mod ((Radix k) |^ u) is_represented_by u,k by Def12;
p = (((Radix k) |^ u) * (p div ((Radix k) |^ u))) + (p mod ((Radix k) |^ u)) by A21, NAT_D:2;
then p = (SDDec (DecSD (p mod ((Radix k) |^ u)),u,k)) + (((Radix k) |^ u) * (p div ((Radix k) |^ u))) by A2, A22;
hence p = SDDec (DecSD p,(u + 1),k) by A8, RVSUM_1:104; :: thesis: verum

end;

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

end;

A23: S₁[1]

proof

let m be Nat; :: thesis: ( m is_represented_by 1,k implies m = SDDec (DecSD m,1,k) )
assume A24: m is_represented_by 1,k ; :: thesis: m = SDDec (DecSD m,1,k)
A25: m is Element of INT by INT_1:def 2;
then reconsider M = <*m*> as FinSequence of INT by FINSEQ_1:95;
A26: 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 A24, Th24 ;
then (DigitSD (DecSD m,1,k)) /. 1 = m by A26, Def6;
hence SDDec (DecSD m,1,k) = Sum M by Th20
.= m by A25, FINSOP_1:12 ;
:: thesis: verum

end;

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