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: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume that
A2: n >= 1 and
A3: S₁[n] ; :: thesis:
let q be Integer; :: thesis:
let ic, f, k be Nat; :: thesis:
assume that
A4: ic is_represented_by n + 1,k and
A5: f > 0 ; :: thesis:
let c be Tuple of n + 1,k -SD ; :: thesis:
deffunc H₁( Nat) -> Element of K556() = DigB c,($1 + 1);
consider cn being FinSequence of INT such that
A6: len cn = n and
A7: for i being Nat st i in dom cn holds
cn . i = H₁(i) from FINSEQ_2:sch 1();
A8: dom cn = Seg n by A6, FINSEQ_1:def 3;
rng cn c= k -SD

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

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 A6, FINSEQ_1:def 18;
A12: n + 1 >= 1 by NAT_1:12;
set c2 = DecSD2 ic,(n + 1),k;
A13: Radix k > 0 by Th6;
deffunc H₂( Nat) -> Element of NAT = (DecSD2 ic,(n + 1),k) . ($1 + 1);
consider cn2 being FinSequence of NAT such that
A14: len cn2 = n and
A15: for i being Nat st i in dom cn2 holds
cn2 . i = H₂(i) from FINSEQ_2:sch 1();
A16: dom cn2 = Seg n by A14, FINSEQ_1:def 3;
reconsider cn2 = cn2 as Tuple of n, NAT by A14, FINSEQ_1:def 18;
set icn2 = SDDec2 cn2,k;
A17: ic < (Radix k) |^ (n + 1) by A4, RADIX_1:def 12;
set icn = SDDec cn;
assume A18: c = DecSD ic,(n + 1),k ; :: thesis:
then A19: DecSD2 ic,(n + 1),k = c by Th14;
A20: for i being Nat st 1 <= i & i <= len cn holds
cn . i = cn2 . i

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i <= len cn ) ; :: thesis:
then A21: i in Seg n by A6, FINSEQ_1:3;
then A22: i + 1 in Seg (n + 1) by Th5;
cn . i = DigB c,(i + 1) by A7, A8, A21
.= DigA c,(i + 1) by RADIX_1:def 4
.= c . (i + 1) by A22, RADIX_1:def 3
.= (DecSD2 ic,(n + 1),k) . (i + 1) by A18, Th14 ;
hence cn . i = cn2 . i by A15, A16, A21; :: thesis:

end;

then A23: SDDec cn = SDDec2 cn2,k by A6, A14, Th13, FINSEQ_1:18;
1 in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
then A24: 1 in Seg (1 + n) by FINSEQ_2:9;
A25: ic = ((Radix k) * (SDDec2 cn2,k)) + ((DecSD2 ic,(n + 1),k) . 1)

proof

A26: len <*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> = 1 by FINSEQ_1:56;
A27: 1 - 1 = 0 ;
deffunc H₃( Nat) -> Element of NAT = (DigitSD2 cn2,k) . $1;
reconsider r2 = Radix k as Element of REAL by XREAL_0:def 1;
consider rD being FinSequence of REAL such that
A28: len rD = n and
A29: 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 A28, FINSEQ_1:def 18;
A30: dom (DigitSD2 cn2,k) = Seg (len (DigitSD2 cn2,k)) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
reconsider rD1 = rD as Element of n -tuples_on REAL by FINSEQ_2:151;
A31: dom rD = Seg n by A28, FINSEQ_1:def 3;
then A32: len ((Radix k) * (DigitSD2 cn2,k)) = len (r2 * rD1) by A29, A30, FINSEQ_1:17
.= n by FINSEQ_1:def 18 ;
A33: 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 A32, FINSEQ_1:def 18 ;
A34: len (DigitSD2 (DecSD2 ic,(n + 1),k),k) = n + 1 by FINSEQ_1:def 18;
A35: 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:
assume that
A36: 1 <= i and
A37: i <= len (DigitSD2 (DecSD2 ic,(n + 1),k),k) ; :: thesis:
A38: i <= n + 1 by A37, FINSEQ_1:def 18;
then A39: i in Seg (n + 1) by A36, FINSEQ_1:3;
then A40: i in dom (DigitSD2 (DecSD2 ic,(n + 1),k),k) by A34, FINSEQ_1:def 3;

per cases ;

suppose A41: i = 1 ; :: thesis:

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 A24, Def2
.= (DigitSD2 (DecSD2 ic,(n + 1),k),k) . 1 by A40, A41, 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 A41; :: thesis:

end;

suppose A42: i <> 1 ; :: thesis:

reconsider rs2 = (DigitSD2 cn2,k) . (i - 1) as Element of NAT ;
reconsider rs = rD . (i - 1) as Real ;
1 - 1 <= i - 1 by A36, XREAL_1:11;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
1 < i by A36, A42, XXREAL_0:1;
then 1 + 1 <= i by INT_1:20;
then A43: (1 + 1) - 1 <= i - 1 by XREAL_1:11;
i - 1 <= (n + 1) - 1 by A38, XREAL_1:11;
then A44: i1 in Seg n by A43, FINSEQ_1:3;
1 < i by A36, A42, 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 A26, A33, A38, FINSEQ_1:37
.= (r2 * rD) . (i - 1) by A29, A30, A31, FINSEQ_1:17
.= r2 * rs by RVSUM_1:67
.= (Radix k) * rs2 by A29, A30, A31, FINSEQ_1:17
.= (Radix k) * ((DigitSD2 cn2,k) /. i1) by A30, A44, PARTFUN1:def 8
.= (Radix k) * (SubDigit2 cn2,i1,k) by A44, 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 A43, XREAL_1:237
.= ((Radix k) |^ i1) * ((DecSD2 ic,(n + 1),k) . (i1 + 1)) by A15, A16, A44
.= SubDigit2 (DecSD2 ic,(n + 1),k),i,k by A36, XREAL_1:235
.= (DigitSD2 (DecSD2 ic,(n + 1),k),k) /. i by A39, 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 A40, PARTFUN1:def 8; :: thesis:

end;

len (DigitSD2 (DecSD2 ic,(n + 1),k),k) = len (<*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k))) by A33, FINSEQ_1:def 18;
then A45: DigitSD2 (DecSD2 ic,(n + 1),k),k = <*(SubDigit2 (DecSD2 ic,(n + 1),k),1,k)*> ^ ((Radix k) * (DigitSD2 cn2,k)) by A35, FINSEQ_1:18;
ic = SDDec2 (DecSD2 ic,(n + 1),k),k by A4, Th15, NAT_1:12
.= (SubDigit2 (DecSD2 ic,(n + 1),k),1,k) + (Sum ((Radix k) * (DigitSD2 cn2,k))) by A45, RVSUM_1:106
.= (SubDigit2 (DecSD2 ic,(n + 1),k),1,k) + (Sum (r2 * rD)) by A29, A30, A31, 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 A29, A30, A31, FINSEQ_1:17
.= (((Radix k) |^ 0 ) * ((DecSD2 ic,(n + 1),k) . 1)) + ((Radix k) * (SDDec2 cn2,k)) by A27, 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:

end;

then A46: (q * ic) mod f = (((q * (Radix k)) * (SDDec2 cn2,k)) + (q * ((DecSD2 ic,(n + 1),k) . 1))) mod f
.= ((((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 A5, Th3
.= (((Radix k) * ((q * (SDDec2 cn2,k)) mod f)) + ((q * ((DecSD2 ic,(n + 1),k) . 1)) mod f)) mod f by A5, Th2 ;
A47: cn = cn2 by A6, A14, A20, FINSEQ_1:18;
A48: for i being Nat st 1 <= i & i <= len cn holds
cn . i = (DecSD2 (SDDec2 cn2,k),n,k) . i

proof

A49: (DecSD2 ic,(n + 1),k) . 1 = DigitDC2 ic,1,k by A24, 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 ;
A50: 0 < Radix k by Th6;
A51: (((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 A50, 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 A13, A49, NAT_D:1, NAT_D:27 ;
A52: Radix k <> 0 by Th6;
let i be Nat; :: thesis:
assume that
A53: 1 <= i and
A54: i <= len cn ; :: thesis:
A55: i in Seg n by A6, A53, A54, FINSEQ_1:3;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A56: 1 <= i + 1 by A53, XREAL_1:31;
( 1 <= i + 1 & i + 1 <= n + 1 ) by A6, A53, A54, XREAL_1:8, XREAL_1:31;
then A57: i + 1 in Seg (n + 1) by FINSEQ_1:3;
cn . i = (DecSD2 ic,(n + 1),k) . (i + 1) by A15, A16, A47, A55
.= DigitDC2 ic,(i + 1),k by A57, Def5
.= ((((SDDec2 cn2,k) * (Radix k)) + ((DecSD2 ic,(n + 1),k) . 1)) div ((Radix k) |^ ((i + 1) -' 1))) mod (Radix k) by A25, A56, Th4, Th6
.= ((((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 A53, A52, PEPIN:27
.= ((SDDec2 cn2,k) div ((Radix k) |^ (i -' 1))) mod (Radix k) by A51, NAT_2:29
.= DigitDC2 (SDDec2 cn2,k),i,k by A53, Th4, Th6 ;
hence cn . i = (DecSD2 (SDDec2 cn2,k),n,k) . i by A55, Def5; :: thesis:

end;

reconsider icn = SDDec cn as Element of NAT by A23;
len cn = len (DecSD2 (SDDec2 cn2,k),n,k) by A6, FINSEQ_1:def 18;
then cn = DecSD2 (SDDec2 cn2,k),n,k by A48, FINSEQ_1:18;
then A58: cn = DecSD icn,n,k by A23, Th14;
ic >= (Radix k) * (SDDec2 cn2,k) by A25, INT_1:19;
then (SDDec2 cn2,k) * (Radix k) < (Radix k) |^ (n + 1) by A17, XXREAL_0:2;
then (SDDec2 cn2,k) * (Radix k) < ((Radix k) |^ n) * (Radix k) by NEWTON:11;
then icn < (Radix k) |^ n by A23, XREAL_1:66;
then A59: icn is_represented_by n,k by RADIX_1:def 12;
A60: 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:
assume A61: i in Seg n ; :: thesis:
DigA c,(i + 1) = DigB c,(i + 1) by RADIX_1:def 4
.= cn . i by A7, A8, A61 ;
hence DigA cn,i = DigA c,(i + 1) by A61, RADIX_1:def 3; :: thesis:

end;

A62: 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 );
A63: for i being Element of NAT st S₂[i] holds
S₂[i + 1]

proof

let i be Element of NAT ; :: thesis:
assume A64: ( i in Seg n implies (Mul_mod q,cn,f,k) . i = (Mul_mod q,c,f,k) . i ) ; :: thesis:
A65: ( i = 0 or i + 1 > 1 + 0 ) by XREAL_1:8;
assume i + 1 in Seg n ; :: thesis:
then A66: i + 1 <= n by FINSEQ_1:3;
then A67: (i + 1) - 1 <= n - 1 by XREAL_1:11;
A68: n in Seg n by A2, FINSEQ_1:3;

now

per cases by A65, NAT_1:13;

case A69: i = 0 ; :: thesis:

then (Mul_mod q,cn,f,k) . (i + 1) = Table1 q,cn,f,n by A2, Def7
.= Table1 q,c,f,(n + 1) by A60, A68
.= (Mul_mod q,c,f,k) . 1 by A12, Def7 ;
hence (Mul_mod q,cn,f,k) . (i + 1) = (Mul_mod q,c,f,k) . (i + 1) by A69; :: thesis:

end;

case A70: i >= 1 ; :: thesis:

reconsider nn = n - 1 as Element of NAT by A2, INT_1:18;
A71: i <= nn + 1 by A67, NAT_1:12;
then i <= (n + 1) - 1 ;
then A72: 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 A12, A70, Def7;
A73: n -' i <= n by NAT_D:35;
(1 + i) - i <= n - i by A66, XREAL_1:11;
then 1 <= n -' i by A71, XREAL_1:235;
then A74: n -' i in Seg n by A73, FINSEQ_1:3;
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 A2, A67, A70, Def7;
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 A60, A64, A70, A71, A74, FINSEQ_1:3
.= (Mul_mod q,c,f,k) . (i + 1) by A71, A72, NAT_D:38 ;
hence (Mul_mod q,cn,f,k) . (i + 1) = (Mul_mod q,c,f,k) . (i + 1) ; :: thesis:

end;

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

end;

A75: S₂[ 0 ] by FINSEQ_1:3;
for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A75, A63);
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:

end;

( n <= (n + 1) - 1 & n + 1 >= 1 ) by NAT_1:11;
then A76: 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 A2, Def7;
n in Seg n by A2, FINSEQ_1:5;
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 A62, A76
.= (((Radix k) * ((q * icn) mod f)) + (Table1 q,c,f,((n + 1) -' n))) mod f by A3, A5, A59, A58
.= (((Radix k) * ((q * (SDDec2 cn2,k)) mod f)) + (Table1 q,c,f,((n + 1) -' n))) mod f by A6, A14, A20, Th13, FINSEQ_1:18
.= (((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 A19, A24, RADIX_1:def 3 ;
hence (Mul_mod q,c,f,k) . (n + 1) = (q * ic) mod f by A46; :: thesis:

end;

A77: S₁[1]

proof

let q be Integer; :: thesis:
let ic, f, k be Nat; :: thesis:
assume that
A78: ic is_represented_by 1,k and
f > 0 ; :: thesis:
let c be Tuple of 1,k -SD ; :: thesis:
assume A79: c = DecSD ic,1,k ; :: thesis:
(Mul_mod q,c,f,k) . 1 = Table1 q,c,f,1 by Def7
.= (q * (SDDec (DecSD ic,1,k))) mod f by A79, Th7 ;
hence (Mul_mod q,c,f,k) . 1 = (q * ic) mod f by A78, RADIX_1:25; :: thesis:

end;

for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A77, A1);
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: