defpred S₁[ Nat] means for q being Integer
for ic, f, k being Nat st ic is_represented_by $1,k & f > 0 holds
for c being Tuple of $1,(k -SD ) st c = DecSD ic,$1,k holds
(Mul_mod q,c,f,k) . $1 = (q * ic) mod f;
A1: S₁[1]

proof

let q be Integer; :: thesis: for ic, f, k being Nat st ic is_represented_by 1,k & f > 0 holds
for c being Tuple of 1,(k -SD ) st c = DecSD ic,1,k holds
(Mul_mod q,c,f,k) . 1 = (q * ic) mod f
let ic, f, k be Nat; :: thesis: ( ic is_represented_by 1,k & f > 0 implies for c being Tuple of 1,(k -SD ) st c = DecSD ic,1,k holds
(Mul_mod q,c,f,k) . 1 = (q * ic) mod f )
assume A2: ( ic is_represented_by 1,k & f > 0 ) ; :: thesis: for c being Tuple of 1,(k -SD ) st c = DecSD ic,1,k holds
(Mul_mod q,c,f,k) . 1 = (q * ic) mod f
let c be Tuple of 1,(k -SD ); :: thesis: ( c = DecSD ic,1,k implies (Mul_mod q,c,f,k) . 1 = (q * ic) mod f )
assume A3: c = DecSD ic,1,k ; :: thesis: (Mul_mod q,c,f,k) . 1 = (q * ic) mod f
(Mul_mod q,c,f,k) . 1 = Table1 q,c,f,1 by Def7
.= (q * (SDDec (DecSD ic,1,k))) mod f by A3, Th7 ;
hence (Mul_mod q,c,f,k) . 1 = (q * ic) mod f by A2, RADIX_1:25; :: thesis: verum

end;

A4: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume A5: ( n >= 1 & S₁[n] ) ; :: thesis: S₁[n + 1]
A6: n + 1 >= 1 by NAT_1:12;
let q be Integer; :: thesis: for ic, f, k being Nat st ic is_represented_by n + 1,k & f > 0 holds
for c being Tuple of (n + 1),(k -SD ) st c = DecSD ic,(n + 1),k holds
(Mul_mod q,c,f,k) . (n + 1) = (q * ic) mod f
let ic, f, k be Nat; :: thesis: ( ic is_represented_by n + 1,k & f > 0 implies for c being Tuple of (n + 1),(k -SD ) st c = DecSD ic,(n + 1),k holds
(Mul_mod q,c,f,k) . (n + 1) = (q * ic) mod f )
assume A7: ( ic is_represented_by n + 1,k & f > 0 ) ; :: thesis: for c being Tuple of (n + 1),(k -SD ) st c = DecSD ic,(n + 1),k holds
(Mul_mod q,c,f,k) . (n + 1) = (q * ic) mod f
let c be Tuple of (n + 1),(k -SD ); :: thesis: ( c = DecSD ic,(n + 1),k implies (Mul_mod q,c,f,k) . (n + 1) = (q * ic) mod f )
assume A8: c = DecSD ic,(n + 1),k ; :: thesis: (Mul_mod q,c,f,k) . (n + 1) = (q * ic) mod f
set c2 = DecSD2 ic,(n + 1),k;
A9: DecSD2 ic,(n + 1),k = c by A8, Th14;
deffunc H₁( Nat) -> Element of K485() = DigB c,($1 + 1);
consider cn being FinSequence of INT such that
A10: len cn = n and
A11: for i being Nat st i in dom cn holds
cn . i = H₁(i) from FINSEQ_2:sch 1();
A12: dom cn = Seg n by A10, FINSEQ_1:def 3;
rng cn c= k -SD

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng cn or z in k -SD )
assume z in rng cn ; :: thesis: z in k -SD
then consider xx being set such that
A13: xx in dom cn and
A14: z = cn . xx by FUNCT_1:def 5;
reconsider xx = xx as Element of NAT by A13;
A15: dom cn = Seg n by A10, FINSEQ_1:def 3;
A16: z = DigB c,(xx + 1) by A11, A13, A14
.= DigA c,(xx + 1) by RADIX_1:def 4 ;
xx + 1 in Seg (n + 1) by A13, A15, Th5;
then DigA c,(xx + 1) is Element of k -SD by RADIX_1:19;
hence z in k -SD by A16; :: thesis: verum

end;

then reconsider cn = cn as FinSequence of k -SD by FINSEQ_1:def 4;
reconsider cn = cn as Tuple of n,(k -SD ) by A10, FINSEQ_2:110;
deffunc H₂( Nat) -> Element of NAT = (DecSD2 ic,(n + 1),k) . ($1 + 1);
consider cn2 being FinSequence of NAT such that
A17: len cn2 = n and
A18: for i being Nat st i in dom cn2 holds
cn2 . i = H₂(i) from FINSEQ_2:sch 1();
A19: dom cn2 = Seg n by A17, FINSEQ_1:def 3;
reconsider cn2 = cn2 as Tuple of n,NAT by A17, FINSEQ_2:110;
A20: for i being Element of NAT st i in Seg n holds
DigA cn,i = DigA c,(i + 1)

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies DigA cn,i = DigA c,(i + 1) )
assume A21: i in Seg n ; :: thesis: DigA cn,i = DigA c,(i + 1)
DigA c,(i + 1) = DigB c,(i + 1) by RADIX_1:def 4
.= cn . i by A11, A21, A12 ;
hence DigA cn,i = DigA c,(i + 1) by A21, RADIX_1:def 3; :: thesis: verum

end;

A22: cn = cn2

proof

for i being Nat st 1 <= i & i <= len cn holds
cn . i = cn2 . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len cn implies cn . i = cn2 . i )
assume ( 1 <= i & i <= len cn ) ; :: thesis: cn . i = cn2 . i
then A23: i in Seg n by A10, FINSEQ_1:3;
then A24: i + 1 in Seg (n + 1) by Th5;
cn . i = DigB c,(i + 1) by A11, A23, A12
.= DigA c,(i + 1) by RADIX_1:def 4
.= c . (i + 1) by A24, RADIX_1:def 3
.= (DecSD2 ic,(n + 1),k) . (i + 1) by A8, Th14 ;
hence cn . i = cn2 . i by A18, A23, A19; :: thesis: verum

end;

hence cn = cn2 by A10, A17, FINSEQ_1:18; :: thesis: verum

end;

1 in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
then A25: 1 in Seg (1 + n) by FINSEQ_2:9;
A26: for i being Element of NAT st i in Seg n holds
(Mul_mod q,cn,f,k) . i = (Mul_mod q,c,f,k) . i

proof

defpred S₂[ Element of NAT ] means ( $1 in Seg n implies (Mul_mod q,cn,f,k) . $1 = (Mul_mod q,c,f,k) . $1 );
A27: S₂[ 0 ] by FINSEQ_1:3;
A28: for i being Element of NAT st S₂[i] holds
S₂[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A29: ( i in Seg n implies (Mul_mod q,cn,f,k) . i = (Mul_mod q,c,f,k) . i ) ; :: thesis: S₂[i + 1]
assume A30: i + 1 in Seg n ; :: thesis: (Mul_mod q,cn,f,k) . (i + 1) = (Mul_mod q,c,f,k) . (i + 1)
A31: n in Seg n by A5, FINSEQ_1:3;
A32: ( 1 <= i + 1 & i + 1 <= n ) by A30, FINSEQ_1:3;
then A33: (i + 1) - 1 <= n - 1 by XREAL_1:11;
A34: ( i = 0 or i + 1 > 1 + 0 ) by XREAL_1:8;

now

per cases ( i = 0 or i >= 1 ) by A34, NAT_1:13;

case A35: i = 0 ; :: thesis: (Mul_mod q,cn,f,k) . (i + 1) = (Mul_mod q,c,f,k) . (i + 1)

then (Mul_mod q,cn,f,k) . (i + 1) = Table1 q,cn,f,n by A5, Def7
.= Table1 q,c,f,(n + 1) by A20, A31
.= (Mul_mod q,c,f,k) . 1 by A6, Def7 ;
hence (Mul_mod q,cn,f,k) . (i + 1) = (Mul_mod q,c,f,k) . (i + 1) by A35; :: thesis: verum

end;

case A36: i >= 1 ; :: thesis: (Mul_mod q,cn,f,k) . (i + 1) = (Mul_mod q,c,f,k) . (i + 1)

reconsider nn = n - 1 as Element of NAT by A5, INT_1:18;
A37: ( 1 <= i & i <= nn + 1 ) by A33, A36, NAT_1:12;
then A38: ( 1 <= i & i <= (n + 1) - 1 ) ;
A39: ex I1, I2 being Integer st
( I1 = (Mul_mod q,cn,f,k) . i & I2 = (Mul_mod q,cn,f,k) . (i + 1) & I2 = (((Radix k) * I1) + (Table1 q,cn,f,(n -' i))) mod f ) by A5, A33, A36, Def7;
A40: ex I1, I2 being Integer st
( I1 = (Mul_mod q,c,f,k) . i & I2 = (Mul_mod q,c,f,k) . (i + 1) & I2 = (((Radix k) * I1) + (Table1 q,c,f,((n + 1) -' i))) mod f ) by A6, A38, Def7;
(1 + i) - i <= n - i by A32, XREAL_1:11;
then A41: 1 <= n -' i by A37, XREAL_1:235;
n -' i <= n by NAT_D:35;
then n -' i in Seg n by A41, FINSEQ_1:3;
then (Mul_mod q,cn,f,k) . (i + 1) = (((Radix k) * ((Mul_mod q,c,f,k) . i)) + ((q * (DigA c,((n -' i) + 1))) mod f)) mod f by A20, A29, A37, A39, FINSEQ_1:3
.= (Mul_mod q,c,f,k) . (i + 1) by A37, A40, NAT_D:38 ;
hence (Mul_mod q,cn,f,k) . (i + 1) = (Mul_mod q,c,f,k) . (i + 1) ; :: thesis: verum

end;

end;

end;

hence (Mul_mod q,cn,f,k) . (i + 1) = (Mul_mod q,c,f,k) . (i + 1) ; :: thesis: verum

end;

for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A27, A28);
hence for i being Element of NAT st i in Seg n holds
(Mul_mod q,cn,f,k) . i = (Mul_mod q,c,f,k) . i ; :: thesis: verum

end;

A42: n in Seg n by A5, FINSEQ_1:5;
set icn = SDDec cn;
set icn2 = SDDec2 cn2,k;
A43: SDDec cn = SDDec2 cn2,k by A22, Th13;
A44: ic = ((Radix k) * (SDDec2 cn2,k)) + ((DecSD2 ic,(n + 1),k) . 1)

proof

reconsider r2 = Radix k as Element of REAL by XREAL_0:def 1;
deffunc H₃( Nat) -> Element of NAT = (DigitSD2 cn2,k) . $1;
consider rD being FinSequence of REAL such that
A45: len rD = n and
A46: for i being Nat st i in dom rD holds
rD . i = H₃(i) from FINSEQ_2:sch 1();
reconsider rD = rD as Tuple of n,REAL by A45, FINSEQ_2:110;
A48: dom (DigitSD2 cn2,k) = Seg (len (DigitSD2 cn2,k)) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
A49: dom rD = Seg n by A45, FINSEQ_1:def 3;
A50: 1 - 1 = 0 ;
A51: DigitSD2 (DecSD2 ic,(n + 1),k),k = <*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))

proof

A52: len (DigitSD2 (DecSD2 ic,(n + 1),k),k) = n + 1 by FINSEQ_1:def 18;
A53: len ((Radix k) * (DigitSD2 cn2,k)) = len (r2 * rD) by A46, A48, A49, FINSEQ_1:17
.= n by FINSEQ_1:def 18 ;
A54: len <*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> = 1 by FINSEQ_1:56;
A55: len (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) = (len <*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*>) + (len ((Radix k) * (DigitSD2 cn2,k))) by FINSEQ_1:35
.= n + 1 by A53, FINSEQ_1:def 18 ;
then A56: len (DigitSD2 (DecSD2 ic,(n + 1),k),k) = len (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) by FINSEQ_1:def 18;
for i being Nat st 1 <= i & i <= len (DigitSD2 (DecSD2 ic,(n + 1),k),k) holds
(DigitSD2 (DecSD2 ic,(n + 1),k),k) . i = (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (DigitSD2 (DecSD2 ic,(n + 1),k),k) implies (DigitSD2 (DecSD2 ic,(n + 1),k),k) . i = (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) . i )
assume A57: ( 1 <= i & i <= len (DigitSD2 (DecSD2 ic,(n + 1),k),k) ) ; :: thesis: (DigitSD2 (DecSD2 ic,(n + 1),k),k) . i = (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) . i
then A58: i <= n + 1 by FINSEQ_1:def 18;
then A59: i in Seg (n + 1) by A57, FINSEQ_1:3;
then A60: i in dom (DigitSD2 (DecSD2 ic,(n + 1),k),k) by A52, FINSEQ_1:def 3;

per cases ( i = 1 or i <> 1 ) ;

suppose A61: i = 1 ; :: thesis: (DigitSD2 (DecSD2 ic,(n + 1),k),k) . i = (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) . i

then (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) . i = SubDigit2 (DecSD2 ic,(n + 1),k),1,k by FINSEQ_1:58
.= (DigitSD2 (DecSD2 ic,(n + 1),k),k) /. 1 by A25, Def2
.= (DigitSD2 (DecSD2 ic,(n + 1),k),k) . 1 by A60, A61, PARTFUN1:def 8 ;
hence (DigitSD2 (DecSD2 ic,(n + 1),k),k) . i = (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) . i by A61; :: thesis: verum

end;

suppose A62: i <> 1 ; :: thesis: (DigitSD2 (DecSD2 ic,(n + 1),k),k) . i = (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) . i

1 - 1 <= i - 1 by A57, XREAL_1:11;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
1 < i by A57, A62, XXREAL_0:1;
then 1 + 1 <= i by INT_1:20;
then A63: (1 + 1) - 1 <= i - 1 by XREAL_1:11;
i - 1 <= (n + 1) - 1 by A58, XREAL_1:11;
then A64: i1 in Seg n by A63, FINSEQ_1:3;
reconsider rs = rD . (i - 1) as Real ;
reconsider rs2 = (DigitSD2 cn2,k) . (i - 1) as Element of NAT ;
1 < i by A57, A62, XXREAL_0:1;
then (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) . i = ((Radix k) * (DigitSD2 cn2,k)) . (i - 1) by A54, A55, A58, FINSEQ_1:37
.= (r2 * rD) . (i - 1) by A46, A48, A49, FINSEQ_1:17
.= r2 * rs by RVSUM_1:67
.= (Radix k) * rs2 by A46, A48, A49, FINSEQ_1:17
.= (Radix k) * ((DigitSD2 cn2,k) /. i1) by A48, A64, PARTFUN1:def 8
.= (Radix k) * (SubDigit2 cn2,i1,k) by A64, Def2
.= ((Radix k) * ((Radix k) |^ (i1 -' 1))) * (cn2 . i1)
.= ((Radix k) |^ ((i1 -' 1) + 1)) * (cn2 . i1) by NEWTON:11
.= ((Radix k) |^ i1) * (cn2 . i1) by A63, XREAL_1:237
.= ((Radix k) |^ i1) * ((DecSD2 ic,(n + 1),k) . (i1 + 1)) by A18, A64, A19
.= SubDigit2 (DecSD2 ic,(n + 1),k),i,k by A57, XREAL_1:235
.= (DigitSD2 (DecSD2 ic,(n + 1),k),k) /. i by A59, Def2 ;
hence (DigitSD2 (DecSD2 ic,(n + 1),k),k) . i = (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) . i by A60, PARTFUN1:def 8; :: thesis: verum

end;

end;

end;

hence DigitSD2 (DecSD2 ic,(n + 1),k),k = <*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k)) by A56, FINSEQ_1:18; :: thesis: verum

end;

ic = SDDec2 (DecSD2 ic,(n + 1),k),k by A7, Th15, NAT_1:12
.= (SubDigit2 (DecSD2 ic,(n + 1),k),1,k) + (Sum ((Radix k) * (DigitSD2 cn2,k))) by A51, RVSUM_1:106
.= (SubDigit2 (DecSD2 ic,(n + 1),k),1,k) + (Sum (r2 * rD)) by A46, A48, A49, FINSEQ_1:17
.= (SubDigit2 (DecSD2 ic,(n + 1),k),1,k) + (r2 * (Sum rD)) by RVSUM_1:117
.= (SubDigit2 (DecSD2 ic,(n + 1),k),1,k) + ((Radix k) * (SDDec2 cn2,k)) by A46, A48, A49, FINSEQ_1:17
.= (((Radix k) |^ 0 ) * ((DecSD2 ic,(n + 1),k) . 1)) + ((Radix k) * (SDDec2 cn2,k)) by A50, XREAL_0:def 2
.= (1 * ((DecSD2 ic,(n + 1),k) . 1)) + ((Radix k) * (SDDec2 cn2,k)) by NEWTON:9 ;
hence ic = ((Radix k) * (SDDec2 cn2,k)) + ((DecSD2 ic,(n + 1),k) . 1) ; :: thesis: verum

end;

reconsider icn = SDDec cn as Element of NAT by A43;
A65: ic >= (Radix k) * (SDDec2 cn2,k) by A44, INT_1:19;
A66: Radix k > 0 by Th6;
ic < (Radix k) |^ (n + 1) by A7, RADIX_1:def 12;
then (SDDec2 cn2,k) * (Radix k) < (Radix k) |^ (n + 1) by A65, XXREAL_0:2;
then (SDDec2 cn2,k) * (Radix k) < ((Radix k) |^ n) * (Radix k) by NEWTON:11;
then icn < (Radix k) |^ n by A43, XREAL_1:66;
then A67: icn is_represented_by n,k by RADIX_1:def 12;
cn = DecSD2 (SDDec2 cn2,k),n,k

proof

A68: len cn = len (DecSD2 (SDDec2 cn2,k),n,k) by A10, FINSEQ_1:def 18;
for i being Nat st 1 <= i & i <= len cn holds
cn . i = (DecSD2 (SDDec2 cn2,k),n,k) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len cn implies cn . i = (DecSD2 (SDDec2 cn2,k),n,k) . i )
assume A69: ( 1 <= i & i <= len cn ) ; :: thesis: cn . i = (DecSD2 (SDDec2 cn2,k),n,k) . i
then A70: i in Seg n by A10, FINSEQ_1:3;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
( 1 <= i + 1 & i + 1 <= n + 1 ) by A10, A69, XREAL_1:8, XREAL_1:31;
then A71: i + 1 in Seg (n + 1) by FINSEQ_1:3;
A72: (DecSD2 ic,(n + 1),k) . 1 = DigitDC2 ic,1,k by A25, Def5
.= (ic mod ((Radix k) |^ 1)) div ((Radix k) |^ 0 ) by XREAL_1:234
.= (ic mod ((Radix k) |^ 1)) div 1 by NEWTON:9
.= ic mod ((Radix k) |^ 1) by NAT_2:6
.= ic mod (Radix k) by NEWTON:10 ;
A73: ( 1 <= i + 1 & 0 < Radix k ) by A69, Th6, XREAL_1:31;
A74: ( Radix k <> 0 & i <> 0 ) by A69, Th6;
A75: (((DecSD2 ic,(n + 1),k) . 1) + ((SDDec2 cn2,k) * (Radix k))) div (Radix k) = [\((((DecSD2 ic,(n + 1),k) . 1) + ((SDDec2 cn2,k) * (Radix k))) / (Radix k))/] by INT_1:def 7
.= [\((((DecSD2 ic,(n + 1),k) . 1) / (Radix k)) + (SDDec2 cn2,k))/] by A73, XCMPLX_1:114
.= [\(((DecSD2 ic,(n + 1),k) . 1) / (Radix k))/] + (SDDec2 cn2,k) by INT_1:51
.= (((DecSD2 ic,(n + 1),k) . 1) div (Radix k)) + (SDDec2 cn2,k) by INT_1:def 7
.= 0 + (SDDec2 cn2,k) by A66, A72, NAT_D:1, NAT_D:27 ;
cn . i = (DecSD2 ic,(n + 1),k) . (i + 1) by A18, A22, A70, A19
.= DigitDC2 ic,(i + 1),k by A71, Def5
.= ((((SDDec2 cn2,k) * (Radix k)) + ((DecSD2 ic,(n + 1),k) . 1)) div ((Radix k) |^ ((i + 1) -' 1))) mod (Radix k) by A44, A73, Th4
.= ((((SDDec2 cn2,k) * (Radix k)) + ((DecSD2 ic,(n + 1),k) . 1)) div ((Radix k) |^ i)) mod (Radix k) by NAT_D:34
.= ((((SDDec2 cn2,k) * (Radix k)) + ((DecSD2 ic,(n + 1),k) . 1)) div ((Radix k) * ((Radix k) |^ (i -' 1)))) mod (Radix k) by A74, PEPIN:27
.= ((SDDec2 cn2,k) div ((Radix k) |^ (i -' 1))) mod (Radix k) by A75, NAT_2:29
.= DigitDC2 (SDDec2 cn2,k),i,k by A69, A73, Th4 ;
hence cn . i = (DecSD2 (SDDec2 cn2,k),n,k) . i by A70, Def5; :: thesis: verum

end;

hence cn = DecSD2 (SDDec2 cn2,k),n,k by A68, FINSEQ_1:18; :: thesis: verum

end;

then A76: cn = DecSD icn,n,k by A43, Th14;
A77: (q * ic) mod f = (((q * (Radix k)) * (SDDec2 cn2,k)) + (q * ((DecSD2 ic,(n + 1),k) . 1))) mod f by A44
.= ((((Radix k) * (q * (SDDec2 cn2,k))) mod f) + ((q * ((DecSD2 ic,(n + 1),k) . 1)) mod f)) mod f by INT_3:14
.= ((((Radix k) * ((q * (SDDec2 cn2,k)) mod f)) mod f) + ((q * ((DecSD2 ic,(n + 1),k) . 1)) mod f)) mod f by A7, Th3
.= (((Radix k) * ((q * (SDDec2 cn2,k)) mod f)) + ((q * ((DecSD2 ic,(n + 1),k) . 1)) mod f)) mod f by A7, Th2 ;
A78: n <= (n + 1) - 1 ;
n + 1 >= 1 by NAT_1:11;
then ex I1, I2 being Integer st
( I1 = (Mul_mod q,c,f,k) . n & I2 = (Mul_mod q,c,f,k) . (n + 1) & I2 = (((Radix k) * I1) + (Table1 q,c,f,((n + 1) -' n))) mod f ) by A5, A78, Def7;
then (Mul_mod q,c,f,k) . (n + 1) = (((Radix k) * ((Mul_mod q,cn,f,k) . n)) + (Table1 q,c,f,((n + 1) -' n))) mod f by A26, A42
.= (((Radix k) * ((q * icn) mod f)) + (Table1 q,c,f,((n + 1) -' n))) mod f by A5, A7, A67, A76
.= (((Radix k) * ((q * (SDDec2 cn2,k)) mod f)) + (Table1 q,c,f,((n + 1) -' n))) mod f by A22, Th13
.= (((Radix k) * ((q * (SDDec2 cn2,k)) mod f)) + ((q * (DigA c,1)) mod f)) mod f by NAT_D:34
.= (((Radix k) * ((q * (SDDec2 cn2,k)) mod f)) + ((q * ((DecSD2 ic,(n + 1),k) . 1)) mod f)) mod f by A9, A25, RADIX_1:def 3 ;
hence (Mul_mod q,c,f,k) . (n + 1) = (q * ic) mod f by A77; :: thesis: verum

end;

for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A1, A4);
hence for n being Nat st n >= 1 holds
for q being Integer
for ic, f, k being Nat st ic is_represented_by n,k & f > 0 holds
for c being Tuple of n,(k -SD ) st c = DecSD ic,n,k holds
(Mul_mod q,c,f,k) . n = (q * ic) mod f ; :: thesis: verum