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 CARD_1:def 7;
A5: 1 <= u + 1 by NAT_1:12;
then A6: u + 1 in Seg (u + 1) by FINSEQ_1:1;
assume p is_represented_by u + 1,k ; :: thesis: p = SDDec (DecSD (p,(u + 1),k))
then p < (Radix k) |^ (u + 1) ;
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:15, 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:74;
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:22
.= u + (len <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*>) by CARD_1:def 7
.= u + 1 by FINSEQ_1:39 ;
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:1;

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

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:1;
then (Radix k) |^ i divides (Radix k) |^ u by NEWTON:89;
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:34;
then t <> 0 by A14, PREPOWER:5;
hence (p mod ((Radix k) |^ u)) mod ((Radix k) |^ i) = p mod ((Radix k) |^ i) by A14, Th3; :: 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 CARD_1:def 7;
then A16: i in dom DD by A11, FINSEQ_1:def 3;
then A17: DD . i = DD /. i by PARTFUN1:def 6;
A18: DD . i = (DigitSD (DecSD (p,(u + 1),k))) /. i by A16, PARTFUN1:def 6
.= 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 CARD_1:def 7;
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 6
.= 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 6; :: thesis: verum

end;

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

hence z /. i = z . (u + 1) by A5, A9, FINSEQ_4:15
.= ((DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ z1) . ((len (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k)))) + 1) by CARD_1:def 7
.= (DigitSD (DecSD (p,(u + 1),k))) . (u + 1) by A7, FINSEQ_1:42
.= DD /. i by A4, A20, FINSEQ_4:15, NAT_1:12 ;
:: thesis: verum

end;

end;

end;

len DD = u + 1 by CARD_1:def 7;
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:13; :: thesis: verum

end;

Radix k <> 0 by POWER:34;
then A21: (Radix k) |^ u <> 0 by PREPOWER:5;
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 ;
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:74; :: 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))
reconsider i = m as Element of REAL by XREAL_0:def 1;
reconsider M = <*i*> as FinSequence of REAL ;
A25: 1 in Seg 1 by FINSEQ_1:1;
SubDigit ((DecSD (m,1,k)),1,k) = ((Radix k) |^ 0) * (DigB ((DecSD (m,1,k)),1)) by XREAL_1:232
.= 1 * (DigB ((DecSD (m,1,k)),1)) by NEWTON:4
.= m by A24, Th20 ;
then (DigitSD (DecSD (m,1,k))) /. 1 = m by A25, Def6;
hence SDDec (DecSD (m,1,k)) = Sum M by Th16
.= m by FINSOP_1:11 ;
:: 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