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 INT = 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 object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng cn ; :: thesis:
then consider xx being object such that
A9: xx in dom cn and
A10: z = cn . xx by FUNCT_1:def 3;
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:16;
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, CARD_1:def 7;
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, CARD_1:def 7;
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:1;
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:14;
1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then A24: 1 in Seg (1 + n) by FINSEQ_2:8;
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:39;
A27: 1 - 1 = 0 ;
deffunc H₃( Nat) -> Element of REAL = In (((DigitSD2 (cn2,k)) . $1),REAL);
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();
A30: for i being Nat st i in dom rD holds
rD . i = (DigitSD2 (cn2,k)) . i

proof

let i be Nat; :: thesis:
assume i in dom rD ; :: thesis:
then rD . i = H₃(i) by A29;
hence rD . i = (DigitSD2 (cn2,k)) . i ; :: thesis:

end;

reconsider rD = rD as Tuple of n, REAL by A28, CARD_1:def 7;
A31: dom (DigitSD2 (cn2,k)) = Seg (len (DigitSD2 (cn2,k))) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7 ;
reconsider rD1 = rD as Element of n -tuples_on REAL by FINSEQ_2:131;
A32: dom rD = Seg n by A28, FINSEQ_1:def 3;
then A33: len ((Radix k) * (DigitSD2 (cn2,k))) = len (r2 * rD1) by A30, A31, FINSEQ_1:13
.= n by CARD_1:def 7 ;
A34: 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:22
.= n + 1 by A33, CARD_1:def 7 ;
A35: len (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) = n + 1 by CARD_1:def 7;
A36: 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
A37: 1 <= i and
A38: i <= len (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) ; :: thesis:
A39: i <= n + 1 by A38, CARD_1:def 7;
then A40: i in Seg (n + 1) by A37, FINSEQ_1:1;
then A41: i in dom (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) by A35, FINSEQ_1:def 3;

per cases ;

suppose A42: 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:41
.= (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) /. 1 by A24, Def2
.= (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) . 1 by A41, A42, PARTFUN1:def 6 ;
hence (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) . i = (<*(SubDigit2 ((DecSD2 (ic,(n + 1),k)),1,k))*> ^ ((Radix k) * (DigitSD2 (cn2,k)))) . i by A42; :: thesis:

end;

suppose A43: 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 A37, XREAL_1:9;
then reconsider i1 = i - 1 as Element of NAT by INT_1:3;
1 < i by A37, A43, XXREAL_0:1;
then 1 + 1 <= i by INT_1:7;
then A44: (1 + 1) - 1 <= i - 1 by XREAL_1:9;
i - 1 <= (n + 1) - 1 by A39, XREAL_1:9;
then A45: i1 in Seg n by A44, FINSEQ_1:1;
1 < i by A37, A43, 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, A34, A39, FINSEQ_1:24
.= (r2 * rD) . (i - 1) by A30, A31, A32, FINSEQ_1:13
.= r2 * rs by RVSUM_1:45
.= (Radix k) * rs2 by A30, A31, A32, FINSEQ_1:13
.= (Radix k) * ((DigitSD2 (cn2,k)) /. i1) by A31, A45, PARTFUN1:def 6
.= (Radix k) * (SubDigit2 (cn2,i1,k)) by A45, Def2
.= ((Radix k) * ((Radix k) |^ (i1 -' 1))) * (cn2 . i1)
.= ((Radix k) |^ ((i1 -' 1) + 1)) * (cn2 . i1) by NEWTON:6
.= ((Radix k) |^ i1) * (cn2 . i1) by A44, XREAL_1:235
.= ((Radix k) |^ i1) * ((DecSD2 (ic,(n + 1),k)) . (i1 + 1)) by A15, A16, A45
.= SubDigit2 ((DecSD2 (ic,(n + 1),k)),i,k) by A37, XREAL_1:233
.= (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) /. i by A40, 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 A41, PARTFUN1:def 6; :: 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 A34, CARD_1:def 7;
then A46: DigitSD2 ((DecSD2 (ic,(n + 1),k)),k) = <*(SubDigit2 ((DecSD2 (ic,(n + 1),k)),1,k))*> ^ ((Radix k) * (DigitSD2 (cn2,k))) by A36, FINSEQ_1:14;
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 A46, RVSUM_1:76
.= (SubDigit2 ((DecSD2 (ic,(n + 1),k)),1,k)) + (Sum (r2 * rD)) by A30, A31, A32, FINSEQ_1:13
.= (SubDigit2 ((DecSD2 (ic,(n + 1),k)),1,k)) + (r2 * (Sum rD)) by RVSUM_1:87
.= (SubDigit2 ((DecSD2 (ic,(n + 1),k)),1,k)) + ((Radix k) * (SDDec2 (cn2,k))) by A30, A31, A32, FINSEQ_1:13
.= (((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:4 ;
hence ic = ((Radix k) * (SDDec2 (cn2,k))) + ((DecSD2 (ic,(n + 1),k)) . 1) ; :: thesis:

end;

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

proof

A50: (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:232
.= (ic mod ((Radix k) |^ 1)) div 1 by NEWTON:4
.= ic mod ((Radix k) |^ 1) by NAT_2:4
.= ic mod (Radix k) ;
A51: 0 < Radix k by Th6;
A52: (((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 9
.= [\((((DecSD2 (ic,(n + 1),k)) . 1) / (Radix k)) + (SDDec2 (cn2,k)))/] by A51, XCMPLX_1:113
.= [\(((DecSD2 (ic,(n + 1),k)) . 1) / (Radix k))/] + (SDDec2 (cn2,k)) by INT_1:28
.= (((DecSD2 (ic,(n + 1),k)) . 1) div (Radix k)) + (SDDec2 (cn2,k)) by INT_1:def 9
.= 0 + (SDDec2 (cn2,k)) by A13, A50, NAT_D:1, NAT_D:27 ;
A53: Radix k <> 0 by Th6;
let i be Nat; :: thesis:
assume that
A54: 1 <= i and
A55: i <= len cn ; :: thesis:
A56: i in Seg n by A6, A54, A55, FINSEQ_1:1;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A57: 1 <= i + 1 by A54, XREAL_1:29;
( 1 <= i + 1 & i + 1 <= n + 1 ) by A6, A54, A55, XREAL_1:6, XREAL_1:29;
then A58: i + 1 in Seg (n + 1) by FINSEQ_1:1;
cn . i = (DecSD2 (ic,(n + 1),k)) . (i + 1) by A15, A16, A48, A56
.= DigitDC2 (ic,(i + 1),k) by A58, Def5
.= ((((SDDec2 (cn2,k)) * (Radix k)) + ((DecSD2 (ic,(n + 1),k)) . 1)) div ((Radix k) |^ ((i + 1) -' 1))) mod (Radix k) by A25, A57, 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 A54, A53, PEPIN:26
.= ((SDDec2 (cn2,k)) div ((Radix k) |^ (i -' 1))) mod (Radix k) by A52, NAT_2:27
.= DigitDC2 ((SDDec2 (cn2,k)),i,k) by A54, Th4, Th6 ;
hence cn . i = (DecSD2 ((SDDec2 (cn2,k)),n,k)) . i by A56, Def5; :: thesis:

end;

reconsider icn = SDDec cn as Element of NAT by A23;
len cn = len (DecSD2 ((SDDec2 (cn2,k)),n,k)) by A6, CARD_1:def 7;
then cn = DecSD2 ((SDDec2 (cn2,k)),n,k) by A49, FINSEQ_1:14;
then A59: cn = DecSD (icn,n,k) by A23, Th14;
ic >= (Radix k) * (SDDec2 (cn2,k)) by A25, INT_1:6;
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:6;
then icn < (Radix k) |^ n by A23, XREAL_1:64;
then A60: icn is_represented_by n,k by RADIX_1:def 12;
A61: 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 A62: i in Seg n ; :: thesis:
DigA (c,(i + 1)) = DigB (c,(i + 1)) by RADIX_1:def 4
.= cn . i by A7, A8, A62 ;
hence DigA (cn,i) = DigA (c,(i + 1)) by A62, RADIX_1:def 3; :: thesis:

end;

A63: 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₂[ Nat] means ( $1 in Seg n implies (Mul_mod (q,cn,f,k)) . $1 = (Mul_mod (q,c,f,k)) . $1 );
A64: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume A65: ( i in Seg n implies (Mul_mod (q,cn,f,k)) . i = (Mul_mod (q,c,f,k)) . i ) ; :: thesis:
A66: ( i = 0 or i + 1 > 1 + 0 ) by XREAL_1:6;
assume i + 1 in Seg n ; :: thesis:
then A67: i + 1 <= n by FINSEQ_1:1;
then A68: (i + 1) - 1 <= n - 1 by XREAL_1:9;
A69: n in Seg n by A2, FINSEQ_1:1;

now :: thesis:

per cases by A66, NAT_1:13;

case A70: 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 A61, A69
.= (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 A70; :: thesis:

end;

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

reconsider nn = n - 1 as Element of NAT by A2, INT_1:5;
A72: i <= nn + 1 by A68, NAT_1:12;
then i <= (n + 1) - 1 ;
then A73: 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, A71, Def7;
A74: n -' i <= n by NAT_D:35;
(1 + i) - i <= n - i by A67, XREAL_1:9;
then 1 <= n -' i by A72, XREAL_1:233;
then A75: n -' i in Seg n by A74, FINSEQ_1:1;
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, A68, A71, 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 A61, A65, A71, A72, A75, FINSEQ_1:1
.= (Mul_mod (q,c,f,k)) . (i + 1) by A72, A73, 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;

A76: S₂[ 0 ] by FINSEQ_1:1;
for i being Nat holds S₂[i] from NAT_1:sch 2(A76, A64);
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 A77: 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:3;
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 A63, A77
.= (((Radix k) * ((q * icn) mod f)) + (Table1 (q,c,f,((n + 1) -' n)))) mod f by A3, A5, A60, A59
.= (((Radix k) * ((q * (SDDec2 (cn2,k))) mod f)) + (Table1 (q,c,f,((n + 1) -' n)))) mod f by A6, A14, A20, Th13, FINSEQ_1:14
.= (((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 A47; :: thesis:

end;

A78: S₁[1]

proof

let q be Integer; :: thesis:
let ic, f, k be Nat; :: thesis:
assume that
A79: ic is_represented_by 1,k and
f > 0 ; :: thesis:
let c be Tuple of 1,k -SD ; :: thesis:
assume A80: 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 A80, Th7 ;
hence (Mul_mod (q,c,f,k)) . 1 = (q * ic) mod f by A79, RADIX_1:22; :: thesis:

end;

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