:: RADIX_2 semantic presentation

begin

theorem :: RADIX_2:1
for a being Nat holds a mod 1 = 0
proof
let a be Nat; ::_thesis: a mod 1 = 0
 a = (1 * a) + 0 ;
hence  a mod 1 = 0 by NAT_D:def_2; ::_thesis: verum
end;

theorem Th2: :: RADIX_2:2
for a, b being Integer
for n being Nat st n > 0 holds
((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n
proof
let a, b be Integer; ::_thesis: for n being Nat st n > 0 holds
((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n
let n be Nat; ::_thesis: ( n > 0 implies ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n )
assume  n > 0 ; ::_thesis: ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n
then (a mod n) + ((a div n) * n) = (a - ((a div n) * n)) + ((a div n) * n) by INT_1:def_10
.= a + 0 ;
then  n divides (a + (b mod n)) - ((a mod n) + (b mod n)) by INT_1:def_3;
then  a + (b mod n),(a mod n) + (b mod n) are_congruent_mod n by INT_2:15;
hence  ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n by NAT_D:64; ::_thesis: verum
end;

theorem Th3: :: RADIX_2:3
for a, b being Integer
for n being Nat st n > 0 holds
(a * b) mod n = (a * (b mod n)) mod n
proof
let a, b be Integer; ::_thesis: for n being Nat st n > 0 holds
(a * b) mod n = (a * (b mod n)) mod n
let n be Nat; ::_thesis: ( n > 0 implies (a * b) mod n = (a * (b mod n)) mod n )
assume  n > 0 ; ::_thesis: (a * b) mod n = (a * (b mod n)) mod n
then (b mod n) + ((b div n) * n) = (b - ((b div n) * n)) + ((b div n) * n) by INT_1:def_10
.= b + 0 ;
then  (a * b) - (a * (b mod n)) = (a * (b div n)) * n ;
then  n divides (a * b) - (a * (b mod n)) by INT_1:def_3;
then  a * b,a * (b mod n) are_congruent_mod n by INT_2:15;
hence  (a * b) mod n = (a * (b mod n)) mod n by NAT_D:64; ::_thesis: verum
end;

theorem Th4: :: RADIX_2:4
for a, b, i being Nat st 1 <= i & 0 < b holds
(a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b
proof
let a, b, i be Nat; ::_thesis: ( 1 <= i & 0 < b implies (a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b )
assume that
A1: 1 <= i and
A2: 0 < b ; ::_thesis: (a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b
set j = i -' 1;
set B0 = b |^ (i -' 1);
A3: b |^ (i -' 1) > 0 by A2, PREPOWER:6;
set B1 = b |^ ((i -' 1) + 1);
A4: a mod (b |^ ((i -' 1) + 1)) = a - ((b |^ ((i -' 1) + 1)) * (a div (b |^ ((i -' 1) + 1)))) by A2, NEWTON:63, PREPOWER:6;
reconsider Z = b * (- (a div (b |^ ((i -' 1) + 1)))) as Integer ;
(i -' 1) + 1 = (i - 1) + 1 by A1, XREAL_1:233
.= i ;
then (a mod (b |^ i)) div (b |^ (i -' 1)) = (a + ((b |^ ((i -' 1) + 1)) * (- (a div (b |^ ((i -' 1) + 1)))))) div (b |^ (i -' 1)) by A4
.= (a + (((b |^ (i -' 1)) * b) * (- (a div (b |^ ((i -' 1) + 1)))))) div (b |^ (i -' 1)) by NEWTON:6
.= [\((a + ((b |^ (i -' 1)) * Z)) / (b |^ (i -' 1)))/] by INT_1:def_9
.= [\((a / (b |^ (i -' 1))) + Z)/] by A3, XCMPLX_1:113
.= [\(a / (b |^ (i -' 1)))/] + Z by INT_1:28
.= (a div (b |^ (i -' 1))) + (- (b * (a div (b |^ ((i -' 1) + 1))))) by INT_1:def_9
.= (a div (b |^ (i -' 1))) - (b * (a div (b |^ ((i -' 1) + 1))))
.= (a div (b |^ (i -' 1))) - (b * (a div ((b |^ (i -' 1)) * b))) by NEWTON:6
.= (a div (b |^ (i -' 1))) - (b * ((a div (b |^ (i -' 1))) div b)) by NAT_2:27 ;
hence  (a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b by A2, NEWTON:63; ::_thesis: verum
end;

theorem Th5: :: RADIX_2:5
for i, n being Nat st i in Seg n holds
i + 1 in Seg (n + 1)
proof
let i, n be Nat; ::_thesis: ( i in Seg n implies i + 1 in Seg (n + 1) )
assume A1: i in Seg n ; ::_thesis: i + 1 in Seg (n + 1)
then  1 <= i by FINSEQ_1:1;
then  1 + 1 <= i + 1 by XREAL_1:6;
then A2: 1 <= i + 1 by XXREAL_0:2;
 i <= n by A1, FINSEQ_1:1;
then  i + 1 <= n + 1 by XREAL_1:6;
hence  i + 1 in Seg (n + 1) by A2, FINSEQ_1:1; ::_thesis: verum
end;

begin

theorem Th6: :: RADIX_2:6
for k being Nat holds Radix k > 0
proof
let k be Nat; ::_thesis: Radix k > 0
 Radix k = 2 to_power k by RADIX_1:def_1;
hence  Radix k > 0 by POWER:34; ::_thesis: verum
end;

theorem Th7: :: RADIX_2:7
for k being Nat
for x being Tuple of 1,k -SD holds SDDec x = DigA (x,1)
proof
let k be Nat; ::_thesis: for x being Tuple of 1,k -SD holds SDDec x = DigA (x,1)
 1 - 1 = 0 ;
then A1: 1 -' 1 = 0 by XREAL_0:def_2;
let x be Tuple of 1,k -SD ; ::_thesis: SDDec x = DigA (x,1)
A2: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1;
then A3: (DigitSD x) /. 1 = SubDigit (x,1,k) by RADIX_1:def_6;
A4: len (DigitSD x) = 1 by CARD_1:def_7;
then  1 in dom (DigitSD x) by A2, FINSEQ_1:def_3;
then A5: (DigitSD x) . 1 = SubDigit (x,1,k) by A3, PARTFUN1:def_6;
thus  SDDec x = Sum (DigitSD x) by RADIX_1:def_7
.= Sum <*(SubDigit (x,1,k))*> by A4, A5, FINSEQ_1:40
.= SubDigit (x,1,k) by RVSUM_1:73
.= ((Radix k) |^ 0) * (DigB (x,1)) by A1, RADIX_1:def_5
.= 1 * (DigB (x,1)) by NEWTON:4
.= DigA (x,1) by RADIX_1:def_4 ; ::_thesis: verum
end;

theorem Th8: :: RADIX_2:8
for k being Nat
for x being Integer holds (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x
proof
let k be Nat; ::_thesis: for x being Integer holds (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x
let x be Integer; ::_thesis: (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x
 (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = (x - ((SD_Add_Carry x) * (Radix k))) + ((SD_Add_Carry x) * (Radix k)) by RADIX_1:def_11;
hence  (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x ; ::_thesis: verum
end;

theorem Th9: :: RADIX_2:9
for k, n being Nat
for x being Tuple of n + 1,k -SD
for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
x . i = xn . i ) holds
Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>)
proof
let k, n be Nat; ::_thesis: for x being Tuple of n + 1,k -SD
for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
x . i = xn . i ) holds
Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>)
let x be Tuple of n + 1,k -SD ; ::_thesis: for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
x . i = xn . i ) holds
Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>)
let xn be Tuple of n,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg n holds
x . i = xn . i ) implies Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) )
A1: len (DigitSD x) = n + 1 by CARD_1:def_7;
assume A2: for i being Nat st i in Seg n holds
x . i = xn . i ; ::_thesis: Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>)
A3: for i being Element of NAT st i in Seg n holds
DigA (x,i) = DigA (xn,i)
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies DigA (x,i) = DigA (xn,i) )
assume A4: i in Seg n ; ::_thesis: DigA (x,i) = DigA (xn,i)
then  i in Seg (n + 1) by FINSEQ_2:8;
then  DigA (x,i) = x . i by RADIX_1:def_3
.= xn . i by A2, A4 ;
hence  DigA (x,i) = DigA (xn,i) by A4, RADIX_1:def_3; ::_thesis: verum
end;
A5: len (DigitSD xn) = n by CARD_1:def_7;
A6: for i being Nat st 1 <= i & i <= len (DigitSD x) holds
(DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (DigitSD x) implies (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i )
assume that
A7: 1 <= i and
A8: i <= len (DigitSD x) ; ::_thesis: (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i
A9: n + 1 in Seg (n + 1) by FINSEQ_1:3;
 i <= n + 1 by A8, CARD_1:def_7;
then A10: i in Seg (n + 1) by A7, FINSEQ_1:1;
now__::_thesis:_(DigitSD_x)_._i_=_((DigitSD_xn)_^_<*(SubDigit_(x,(n_+_1),k))*>)_._i
percases ( i in Seg n or i = n + 1 ) by A10, FINSEQ_2:7;
supposeA11: i in Seg n ; ::_thesis: (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i
then A12: i in Seg (n + 1) by FINSEQ_2:8;
then A13: i in dom (DigitSD x) by A1, FINSEQ_1:def_3;
A14: i in dom (DigitSD xn) by A5, A11, FINSEQ_1:def_3;
then ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i = (DigitSD xn) . i by FINSEQ_1:def_7
.= (DigitSD xn) /. i by A14, PARTFUN1:def_6
.= SubDigit (xn,i,k) by A11, RADIX_1:def_6
.= ((Radix k) |^ (i -' 1)) * (DigB (xn,i)) by RADIX_1:def_5
.= ((Radix k) |^ (i -' 1)) * (DigA (xn,i)) by RADIX_1:def_4
.= ((Radix k) |^ (i -' 1)) * (DigA (x,i)) by A3, A11
.= ((Radix k) |^ (i -' 1)) * (DigB (x,i)) by RADIX_1:def_4
.= SubDigit (x,i,k) by RADIX_1:def_5
.= (DigitSD x) /. i by A12, RADIX_1:def_6 ;
hence  (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i by A13, PARTFUN1:def_6; ::_thesis: verum
end;
supposeA15: i = n + 1 ; ::_thesis: (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i
then A16: i in dom (DigitSD x) by A1, A9, FINSEQ_1:def_3;
((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . ((len (DigitSD xn)) + 1) by A15, CARD_1:def_7
.= SubDigit (x,(n + 1),k) by FINSEQ_1:42
.= (DigitSD x) /. (n + 1) by A9, RADIX_1:def_6
.= (DigitSD x) . (n + 1) by A15, A16, PARTFUN1:def_6 ;
hence  (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i by A15; ::_thesis: verum
end;
end;
end;
hence  (DigitSD x) . i = ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) . i ; ::_thesis: verum
end;
A17: len <*(SubDigit (x,(n + 1),k))*> = 1 by FINSEQ_1:39;
len ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) = (len (DigitSD xn)) + (len <*(SubDigit (x,(n + 1),k))*>) by FINSEQ_1:22
.= n + 1 by A17, CARD_1:def_7 ;
then  len (DigitSD x) = len ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) by CARD_1:def_7;
hence  Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) by A6, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th10: :: RADIX_2:10
for k, n being Nat
for x being Tuple of n + 1,k -SD
for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
x . i = xn . i ) holds
(SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x
proof
let k, n be Nat; ::_thesis: for x being Tuple of n + 1,k -SD
for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
x . i = xn . i ) holds
(SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x
let x be Tuple of n + 1,k -SD ; ::_thesis: for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
x . i = xn . i ) holds
(SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x
let xn be Tuple of n,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg n holds
x . i = xn . i ) implies (SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x )
assume A1: for i being Nat st i in Seg n holds
x . i = xn . i ; ::_thesis: (SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x
SDDec x = Sum (DigitSD x) by RADIX_1:def_7
.= Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>) by A1, Th9
.= (Sum (DigitSD xn)) + (SubDigit (x,(n + 1),k)) by RVSUM_1:74
.= (Sum (DigitSD xn)) + (((Radix k) |^ ((n + 1) -' 1)) * (DigB (x,(n + 1)))) by RADIX_1:def_5
.= (Sum (DigitSD xn)) + (((Radix k) |^ n) * (DigB (x,(n + 1)))) by NAT_D:34
.= (Sum (DigitSD xn)) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) by RADIX_1:def_4 ;
hence  (SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x by RADIX_1:def_7; ::_thesis: verum
end;

theorem :: RADIX_2:11
for k, n being Nat st n >= 1 holds
for x, y being Tuple of n,k -SD st k >= 2 holds
(SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,n)) + (DigA (y,n)))) * ((Radix k) |^ n)) = (SDDec x) + (SDDec y)
proof
let k be Nat; ::_thesis: for n being Nat st n >= 1 holds
for x, y being Tuple of n,k -SD st k >= 2 holds
(SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,n)) + (DigA (y,n)))) * ((Radix k) |^ n)) = (SDDec x) + (SDDec y)
defpred S1[ Nat] means  for x, y being Tuple of $1,k -SD st k >= 2 holds
(SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,$1)) + (DigA (y,$1)))) * ((Radix k) |^ $1)) = (SDDec x) + (SDDec y);
A1: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A2: n >= 1 and
A3: S1[n] ; ::_thesis: S1[n + 1]
A4: n in Seg n by A2, FINSEQ_1:3;
let x, y be Tuple of n + 1,k -SD ; ::_thesis: ( k >= 2 implies (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,(n + 1))) + (DigA (y,(n + 1))))) * ((Radix k) |^ (n + 1))) = (SDDec x) + (SDDec y) )
assume A5: k >= 2 ; ::_thesis: (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,(n + 1))) + (DigA (y,(n + 1))))) * ((Radix k) |^ (n + 1))) = (SDDec x) + (SDDec y)
deffunc H1( Nat) ->  Element of INT = DigB (x,$1);
consider xn being FinSequence of INT  such that
A6: len xn = n and
A7: for i being Nat st i in dom xn holds
xn . i = H1(i) from FINSEQ_2:sch_1();
A8: dom xn = Seg n by A6, FINSEQ_1:def_3;
 rng xn c= k -SD
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng xn or z in k -SD )
assume  z in rng xn ; ::_thesis: z in k -SD
then consider xx being set  such that
A9: xx in dom xn and
A10: z = xn . xx by FUNCT_1:def_3;
reconsider xx = xx as Element of NAT by A9;
 dom xn = Seg n by A6, FINSEQ_1:def_3;
then  xx in Seg (n + 1) by A9, FINSEQ_2:8;
then A11: DigA (x,xx) is Element of k -SD by RADIX_1:16;
z = DigB (x,xx) by A7, A9, A10
.= DigA (x,xx) by RADIX_1:def_4 ;
hence  z in k -SD by A11; ::_thesis: verum
end;
then reconsider xn = xn as FinSequence of k -SD by FINSEQ_1:def_4;
A12: for i being Nat st i in Seg n holds
xn . i = x . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies xn . i = x . i )
assume A13: i in Seg n ; ::_thesis: xn . i = x . i
then A14: i in Seg (n + 1) by FINSEQ_2:8;
xn . i = DigB (x,i) by A7, A8, A13
.= DigA (x,i) by RADIX_1:def_4 ;
hence  xn . i = x . i by A14, RADIX_1:def_3; ::_thesis: verum
end;
reconsider xn = xn as Tuple of n,k -SD by A6, CARD_1:def_7;
deffunc H2( Nat) ->  Element of INT = DigB (y,$1);
consider yn being FinSequence of INT  such that
A15: len yn = n and
A16: for i being Nat st i in dom yn holds
yn . i = H2(i) from FINSEQ_2:sch_1();
A17: dom yn = Seg n by A15, FINSEQ_1:def_3;
 rng yn c= k -SD
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng yn or z in k -SD )
assume  z in rng yn ; ::_thesis: z in k -SD
then consider yy being set  such that
A18: yy in dom yn and
A19: z = yn . yy by FUNCT_1:def_3;
reconsider yy = yy as Element of NAT by A18;
 dom yn = Seg n by A15, FINSEQ_1:def_3;
then  yy in Seg (n + 1) by A18, FINSEQ_2:8;
then A20: DigA (y,yy) is Element of k -SD by RADIX_1:16;
z = DigB (y,yy) by A16, A18, A19
.= DigA (y,yy) by RADIX_1:def_4 ;
hence  z in k -SD by A20; ::_thesis: verum
end;
then reconsider yn = yn as FinSequence of k -SD by FINSEQ_1:def_4;
A21: for i being Nat st i in Seg n holds
yn . i = y . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies yn . i = y . i )
assume A22: i in Seg n ; ::_thesis: yn . i = y . i
then A23: i in Seg (n + 1) by FINSEQ_2:8;
yn . i = DigB (y,i) by A16, A17, A22
.= DigA (y,i) by RADIX_1:def_4 ;
hence  yn . i = y . i by A23, RADIX_1:def_3; ::_thesis: verum
end;
reconsider yn = yn as Tuple of n,k -SD by A15, CARD_1:def_7;
A24: for i being Nat st i in Seg n holds
DigA (y,i) = DigA (yn,i)
proof
let i be Nat; ::_thesis: ( i in Seg n implies DigA (y,i) = DigA (yn,i) )
assume A25: i in Seg n ; ::_thesis: DigA (y,i) = DigA (yn,i)
then  i in Seg (n + 1) by FINSEQ_2:8;
then  DigA (y,i) = y . i by RADIX_1:def_3
.= yn . i by A21, A25 ;
hence  DigA (y,i) = DigA (yn,i) by A25, RADIX_1:def_3; ::_thesis: verum
end;
A26: n + 1 in Seg (n + 1) by FINSEQ_1:3;
A27: for i being Element of NAT st i in Seg n holds
DigA (x,i) = DigA (xn,i)
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies DigA (x,i) = DigA (xn,i) )
assume A28: i in Seg n ; ::_thesis: DigA (x,i) = DigA (xn,i)
then  i in Seg (n + 1) by FINSEQ_2:8;
then  DigA (x,i) = x . i by RADIX_1:def_3
.= xn . i by A12, A28 ;
hence  DigA (x,i) = DigA (xn,i) by A28, RADIX_1:def_3; ::_thesis: verum
end;
 for i being Nat st i in Seg n holds
(x '+' y) . i = (xn '+' yn) . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies (x '+' y) . i = (xn '+' yn) . i )
assume A29: i in Seg n ; ::_thesis: (x '+' y) . i = (xn '+' yn) . i
then A30: i in Seg (n + 1) by FINSEQ_2:8;
 (x '+' y) . i = (xn '+' yn) . i
proof
A31: i <= n + 1 by A30, FINSEQ_1:1;
A32: i >= 1 by A29, FINSEQ_1:1;
now__::_thesis:_(x_'+'_y)_._i_=_(xn_'+'_yn)_._i
percases ( i > 1 or i = 1 ) by A32, XXREAL_0:1;
supposeA33: i > 1 ; ::_thesis: (x '+' y) . i = (xn '+' yn) . i
then  i - 1 > 1 - 1 by XREAL_1:9;
then A34: i -' 1 = i - 1 by XREAL_0:def_2;
 i -' 1 > 1 -' 1 by A33, NAT_D:57;
then A35: i -' 1 >= 1 by NAT_1:14;
 i - 1 <= (n + 1) - 1 by A31, XREAL_1:9;
then A36: i -' 1 in Seg n by A35, A34, FINSEQ_1:1;
(x '+' y) . i = DigA ((x '+' y),i) by A30, RADIX_1:def_3
.= Add (x,y,i,k) by A30, RADIX_1:def_14
.= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) by A5, A30, RADIX_1:def_13
.= (SD_Add_Data (((DigA (xn,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) by A27, A29
.= (SD_Add_Data (((DigA (xn,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (xn,(i -' 1))) + (DigA (y,(i -' 1))))) by A27, A36
.= (SD_Add_Data (((DigA (xn,i)) + (DigA (yn,i))),k)) + (SD_Add_Carry ((DigA (xn,(i -' 1))) + (DigA (y,(i -' 1))))) by A24, A29
.= (SD_Add_Data (((DigA (xn,i)) + (DigA (yn,i))),k)) + (SD_Add_Carry ((DigA (xn,(i -' 1))) + (DigA (yn,(i -' 1))))) by A24, A36
.= Add (xn,yn,i,k) by A5, A29, RADIX_1:def_13
.= DigA ((xn '+' yn),i) by A29, RADIX_1:def_14 ;
hence  (x '+' y) . i = (xn '+' yn) . i by A29, RADIX_1:def_3; ::_thesis: verum
end;
supposeA37: i = 1 ; ::_thesis: (x '+' y) . i = (xn '+' yn) . i
(x '+' y) . i = DigA ((x '+' y),i) by A30, RADIX_1:def_3
.= Add (x,y,i,k) by A30, RADIX_1:def_14
.= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(1 -' 1))) + (DigA (y,(1 -' 1))))) by A5, A30, A37, RADIX_1:def_13
.= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,0)) + (DigA (y,(1 -' 1))))) by XREAL_1:232
.= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,0)) + (DigA (y,0)))) by XREAL_1:232
.= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry (0 + (DigA (y,0)))) by RADIX_1:def_3
.= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry (0 + 0)) by RADIX_1:def_3
.= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (xn,0)) + 0)) by RADIX_1:def_3
.= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (xn,0)) + (DigA (yn,0)))) by RADIX_1:def_3
.= (SD_Add_Data (((DigA (xn,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (xn,0)) + (DigA (yn,0)))) by A27, A29
.= (SD_Add_Data (((DigA (xn,i)) + (DigA (yn,i))),k)) + (SD_Add_Carry ((DigA (xn,0)) + (DigA (yn,0)))) by A24, A29
.= (SD_Add_Data (((DigA (xn,i)) + (DigA (yn,i))),k)) + (SD_Add_Carry ((DigA (xn,(1 -' 1))) + (DigA (yn,0)))) by XREAL_1:232
.= (SD_Add_Data (((DigA (xn,i)) + (DigA (yn,i))),k)) + (SD_Add_Carry ((DigA (xn,(i -' 1))) + (DigA (yn,(i -' 1))))) by A37, XREAL_1:232
.= Add (xn,yn,i,k) by A5, A29, RADIX_1:def_13
.= DigA ((xn '+' yn),i) by A29, RADIX_1:def_14 ;
hence  (x '+' y) . i = (xn '+' yn) . i by A29, RADIX_1:def_3; ::_thesis: verum
end;
end;
end;
hence  (x '+' y) . i = (xn '+' yn) . i ; ::_thesis: verum
end;
hence  (x '+' y) . i = (xn '+' yn) . i ; ::_thesis: verum
end;
then  Sum (DigitSD (x '+' y)) = Sum ((DigitSD (xn '+' yn)) ^ <*(SubDigit ((x '+' y),(n + 1),k))*>) by Th9;
then  SDDec (x '+' y) = Sum ((DigitSD (xn '+' yn)) ^ <*(SubDigit ((x '+' y),(n + 1),k))*>) by RADIX_1:def_7
.= (Sum (DigitSD (xn '+' yn))) + (SubDigit ((x '+' y),(n + 1),k)) by RVSUM_1:74
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ ((n + 1) -' 1)) * (DigB ((x '+' y),(n + 1)))) by RADIX_1:def_5
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * (DigB ((x '+' y),(n + 1)))) by NAT_D:34
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * (DigA ((x '+' y),(n + 1)))) by RADIX_1:def_4
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * (Add (x,y,(n + 1),k))) by A26, RADIX_1:def_14
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * ((SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k)) + (SD_Add_Carry ((DigA (x,((n + 1) -' 1))) + (DigA (y,((n + 1) -' 1))))))) by A5, A26, RADIX_1:def_13
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * ((SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k)) + (SD_Add_Carry ((DigA (x,n)) + (DigA (y,((n + 1) -' 1))))))) by NAT_D:34
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * ((SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k)) + (SD_Add_Carry ((DigA (x,n)) + (DigA (y,n)))))) by NAT_D:34
.= ((Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA (x,n)) + (DigA (y,n)))))) + (((Radix k) |^ n) * (SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k)))
.= ((SDDec (xn '+' yn)) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA (x,n)) + (DigA (y,n)))))) + (((Radix k) |^ n) * (SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k))) by RADIX_1:def_7
.= ((SDDec (xn '+' yn)) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA (xn,n)) + (DigA (y,n)))))) + (((Radix k) |^ n) * (SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k))) by A27, A4
.= ((SDDec (xn '+' yn)) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA (xn,n)) + (DigA (yn,n)))))) + (((Radix k) |^ n) * (SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k))) by A2, A24, FINSEQ_1:3
.= ((SDDec xn) + (SDDec yn)) + (((Radix k) |^ n) * (SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k))) by A3, A5 ;
then (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,(n + 1))) + (DigA (y,(n + 1))))) * ((Radix k) |^ (n + 1))) = ((SDDec xn) + (SDDec yn)) + ((((Radix k) |^ n) * (SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k))) + ((SD_Add_Carry ((DigA (x,(n + 1))) + (DigA (y,(n + 1))))) * ((Radix k) |^ (n + 1))))
.= ((SDDec xn) + (SDDec yn)) + ((((Radix k) |^ n) * (SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k))) + ((SD_Add_Carry ((DigA (x,(n + 1))) + (DigA (y,(n + 1))))) * (((Radix k) |^ n) * (Radix k)))) by NEWTON:6
.= ((SDDec xn) + (SDDec yn)) + (((Radix k) |^ n) * ((SD_Add_Data (((DigA (x,(n + 1))) + (DigA (y,(n + 1)))),k)) + ((SD_Add_Carry ((DigA (x,(n + 1))) + (DigA (y,(n + 1))))) * (Radix k))))
.= ((SDDec xn) + (SDDec yn)) + (((Radix k) |^ n) * ((DigA (x,(n + 1))) + (DigA (y,(n + 1))))) by Th8
.= ((SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1))))) + ((SDDec yn) + (((Radix k) |^ n) * (DigA (y,(n + 1)))))
.= (SDDec x) + ((SDDec yn) + (((Radix k) |^ n) * (DigA (y,(n + 1))))) by A12, Th10 ;
hence  (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,(n + 1))) + (DigA (y,(n + 1))))) * ((Radix k) |^ (n + 1))) = (SDDec x) + (SDDec y) by A21, Th10; ::_thesis: verum
end;
A38: S1[1]
proof
 1 - 1 = 0 ;
then A39: 1 -' 1 = 0 by XREAL_0:def_2;
let x, y be Tuple of 1,k -SD ; ::_thesis: ( k >= 2 implies (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,1)) + (DigA (y,1)))) * ((Radix k) |^ 1)) = (SDDec x) + (SDDec y) )
assume A40: k >= 2 ; ::_thesis: (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,1)) + (DigA (y,1)))) * ((Radix k) |^ 1)) = (SDDec x) + (SDDec y)
A41: ( SDDec y = DigA (y,1) & SD_Add_Data (((DigA (x,1)) + (DigA (y,1))),k) = ((DigA (x,1)) + (DigA (y,1))) - ((SD_Add_Carry ((DigA (x,1)) + (DigA (y,1)))) * (Radix k)) ) by Th7, RADIX_1:def_11;
A42: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1;
then  DigA ((x '+' y),1) = Add (x,y,1,k) by RADIX_1:def_14
.= (SD_Add_Data (((DigA (x,1)) + (DigA (y,1))),k)) + (SD_Add_Carry ((DigA (x,0)) + (DigA (y,0)))) by A40, A42, A39, RADIX_1:def_13
.= (SD_Add_Data (((DigA (x,1)) + (DigA (y,1))),k)) + (SD_Add_Carry (0 + (DigA (y,0)))) by RADIX_1:def_3
.= (SD_Add_Data (((DigA (x,1)) + (DigA (y,1))),k)) + 0 by RADIX_1:18, RADIX_1:def_3 ;
then  SDDec (x '+' y) = SD_Add_Data (((DigA (x,1)) + (DigA (y,1))),k) by Th7;
hence (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,1)) + (DigA (y,1)))) * ((Radix k) |^ 1)) = (SD_Add_Data (((DigA (x,1)) + (DigA (y,1))),k)) + ((SD_Add_Carry ((DigA (x,1)) + (DigA (y,1)))) * (Radix k)) by NEWTON:5
.= (SDDec x) + (SDDec y) by A41, Th7 ;
::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A38, A1);
hence  for n being Nat st n >= 1 holds
for x, y being Tuple of n,k -SD st k >= 2 holds
(SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,n)) + (DigA (y,n)))) * ((Radix k) |^ n)) = (SDDec x) + (SDDec y) ; ::_thesis: verum
end;

begin

definition
let i, k, n be Nat;
let x be Tuple of n, NAT ;
func SubDigit2 (x,i,k) ->  Element of NAT  equals :: RADIX_2:def 1
((Radix k) |^ (i -' 1)) * (x . i);
coherence
 ((Radix k) |^ (i -' 1)) * (x . i) is Element of NAT ;
end;

:: deftheorem  defines SubDigit2 RADIX_2:def_1_:_
 for i, k, n being Nat
for x being Tuple of n, NAT holds SubDigit2 (x,i,k) = ((Radix k) |^ (i -' 1)) * (x . i);

definition
let n, k be Nat;
let x be Tuple of n, NAT ;
func DigitSD2 (x,k) ->  Tuple of n, NAT  means :Def2: :: RADIX_2:def 2
 for i being Nat st i in Seg n holds
it /. i = SubDigit2 (x,i,k);
existence
 ex b1 being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b1 /. i = SubDigit2 (x,i,k)
proof
deffunc H1( Nat) ->  Element of NAT = SubDigit2 (x,$1,k);
consider z being FinSequence of NAT  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
reconsider z = z as Tuple of n, NAT by A1, CARD_1:def_7;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
z /. i = SubDigit2 (x,i,k)
let i be Nat; ::_thesis: ( i in Seg n implies z /. i = SubDigit2 (x,i,k) )
assume A4: i in Seg n ; ::_thesis: z /. i = SubDigit2 (x,i,k)
then  i in dom z by A1, FINSEQ_1:def_3;
hence z /. i = z . i by PARTFUN1:def_6
.= SubDigit2 (x,i,k) by A2, A3, A4 ;
::_thesis: verum
end;
uniqueness
 for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b1 /. i = SubDigit2 (x,i,k) ) & ( for i being Nat st i in Seg n holds
b2 /. i = SubDigit2 (x,i,k) ) holds
b1 = b2
proof
let k1, k2 be Tuple of n, NAT ; ::_thesis: ( ( for i being Nat st i in Seg n holds
k1 /. i = SubDigit2 (x,i,k) ) & ( for i being Nat st i in Seg n holds
k2 /. i = SubDigit2 (x,i,k) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
k1 /. i = SubDigit2 (x,i,k) and
A6: for i being Nat st i in Seg n holds
k2 /. i = SubDigit2 (x,i,k) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: len k2 = n by CARD_1:def_7;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then A11: j in dom k2 by A9, A8, FINSEQ_1:def_3;
k1 . j = k1 /. j by A10, PARTFUN1:def_6
.= SubDigit2 (x,j,k) by A5, A8, A10
.= k2 /. j by A6, A8, A10 ;
hence  k1 . j = k2 . j by A11, PARTFUN1:def_6; ::_thesis: verum
end;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines DigitSD2 RADIX_2:def_2_:_
 for n, k being Nat
for x, b4 being Tuple of n, NAT holds
( b4 = DigitSD2 (x,k) iff for i being Nat st i in Seg n holds
b4 /. i = SubDigit2 (x,i,k) );

definition
let n, k be Nat;
let x be Tuple of n, NAT ;
func SDDec2 (x,k) ->  Element of NAT  equals :: RADIX_2:def 3
 Sum (DigitSD2 (x,k));
coherence
 Sum (DigitSD2 (x,k)) is Element of NAT ;
end;

:: deftheorem  defines SDDec2 RADIX_2:def_3_:_
 for n, k being Nat
for x being Tuple of n, NAT holds SDDec2 (x,k) = Sum (DigitSD2 (x,k));

definition
let i, k, x be Nat;
func DigitDC2 (x,i,k) ->  Element of NAT  equals :: RADIX_2:def 4
(x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));
coherence
 (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of NAT ;
end;

:: deftheorem  defines DigitDC2 RADIX_2:def_4_:_
 for i, k, x being Nat holds DigitDC2 (x,i,k) = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));

definition
let k, n, x be Nat;
func DecSD2 (x,n,k) ->  Tuple of n, NAT  means :Def5: :: RADIX_2:def 5
 for i being Nat st i in Seg n holds
it . i = DigitDC2 (x,i,k);
existence
 ex b1 being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b1 . i = DigitDC2 (x,i,k)
proof
deffunc H1( Nat) ->  Element of NAT = DigitDC2 (x,$1,k);
consider z being FinSequence of NAT  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
reconsider z = z as Tuple of n, NAT by A1, CARD_1:def_7;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
z . i = DigitDC2 (x,i,k)
let i be Nat; ::_thesis: ( i in Seg n implies z . i = DigitDC2 (x,i,k) )
assume  i in Seg n ; ::_thesis: z . i = DigitDC2 (x,i,k)
hence  z . i = DigitDC2 (x,i,k) by A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b1 . i = DigitDC2 (x,i,k) ) & ( for i being Nat st i in Seg n holds
b2 . i = DigitDC2 (x,i,k) ) holds
b1 = b2
proof
let k1, k2 be Tuple of n, NAT ; ::_thesis: ( ( for i being Nat st i in Seg n holds
k1 . i = DigitDC2 (x,i,k) ) & ( for i being Nat st i in Seg n holds
k2 . i = DigitDC2 (x,i,k) ) implies k1 = k2 )
assume that
A4: for i being Nat st i in Seg n holds
k1 . i = DigitDC2 (x,i,k) and
A5: for i being Nat st i in Seg n holds
k2 . i = DigitDC2 (x,i,k) ; ::_thesis: k1 = k2
A6: len k1 = n by CARD_1:def_7;
then A7: dom k1 = Seg n by FINSEQ_1:def_3;
A8: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A9: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then  k1 . j = DigitDC2 (x,j,k) by A4, A7;
hence  k1 . j = k2 . j by A5, A7, A9; ::_thesis: verum
end;
 len k2 = n by CARD_1:def_7;
hence  k1 = k2 by A6, A8, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines DecSD2 RADIX_2:def_5_:_
 for k, n, x being Nat
for b4 being Tuple of n, NAT holds
( b4 = DecSD2 (x,n,k) iff for i being Nat st i in Seg n holds
b4 . i = DigitDC2 (x,i,k) );

theorem Th12: :: RADIX_2:12
for n, k being Nat
for x being Tuple of n, NAT
for y being Tuple of n,k -SD st x = y holds
DigitSD2 (x,k) = DigitSD y
proof
let n, k be Nat; ::_thesis: for x being Tuple of n, NAT
for y being Tuple of n,k -SD st x = y holds
DigitSD2 (x,k) = DigitSD y
let x be Tuple of n, NAT ; ::_thesis: for y being Tuple of n,k -SD st x = y holds
DigitSD2 (x,k) = DigitSD y
let y be Tuple of n,k -SD ; ::_thesis: ( x = y implies DigitSD2 (x,k) = DigitSD y )
A1: len (DigitSD y) = n by CARD_1:def_7;
A2: len (DigitSD2 (x,k)) = n by CARD_1:def_7;
then A3: dom (DigitSD2 (x,k)) = Seg n by FINSEQ_1:def_3;
assume A4: x = y ; ::_thesis: DigitSD2 (x,k) = DigitSD y
A5: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
x_._i_=_DigB_(y,i)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies x . i = DigB (y,i) )
assume  i in Seg n ; ::_thesis: x . i = DigB (y,i)
then x . i = DigA (y,i) by A4, RADIX_1:def_3
.= DigB (y,i) by RADIX_1:def_4 ;
hence  x . i = DigB (y,i) ; ::_thesis: verum
end;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_(DigitSD2_(x,k))_holds_
(DigitSD2_(x,k))_._j_=_(DigitSD_y)_._j
let j be Nat; ::_thesis: ( j in dom (DigitSD2 (x,k)) implies (DigitSD2 (x,k)) . j = (DigitSD y) . j )
assume A6: j in dom (DigitSD2 (x,k)) ; ::_thesis: (DigitSD2 (x,k)) . j = (DigitSD y) . j
then A7: j in dom (DigitSD y) by A1, A3, FINSEQ_1:def_3;
(DigitSD2 (x,k)) . j = (DigitSD2 (x,k)) /. j by A6, PARTFUN1:def_6
.= SubDigit2 (x,j,k) by A3, A6, Def2
.= ((Radix k) |^ (j -' 1)) * (DigB (y,j)) by A5, A3, A6
.= SubDigit (y,j,k) by RADIX_1:def_5
.= (DigitSD y) /. j by A3, A6, RADIX_1:def_6
.= (DigitSD y) . j by A7, PARTFUN1:def_6 ;
hence  (DigitSD2 (x,k)) . j = (DigitSD y) . j ; ::_thesis: verum
end;
hence  DigitSD2 (x,k) = DigitSD y by A2, A1, FINSEQ_2:9; ::_thesis: verum
end;

theorem Th13: :: RADIX_2:13
for n, k being Nat
for x being Tuple of n, NAT
for y being Tuple of n,k -SD st x = y holds
SDDec2 (x,k) = SDDec y
proof
let n, k be Nat; ::_thesis: for x being Tuple of n, NAT
for y being Tuple of n,k -SD st x = y holds
SDDec2 (x,k) = SDDec y
let x be Tuple of n, NAT ; ::_thesis: for y being Tuple of n,k -SD st x = y holds
SDDec2 (x,k) = SDDec y
let y be Tuple of n,k -SD ; ::_thesis: ( x = y implies SDDec2 (x,k) = SDDec y )
assume  x = y ; ::_thesis: SDDec2 (x,k) = SDDec y
then  SDDec2 (x,k) = Sum (DigitSD y) by Th12;
hence  SDDec2 (x,k) = SDDec y by RADIX_1:def_7; ::_thesis: verum
end;

theorem Th14: :: RADIX_2:14
for x, n, k being Nat holds DecSD2 (x,n,k) = DecSD (x,n,k)
proof
let x, n, k be Nat; ::_thesis: DecSD2 (x,n,k) = DecSD (x,n,k)
A1: len (DecSD2 (x,n,k)) = n by CARD_1:def_7;
then A2: dom (DecSD2 (x,n,k)) = Seg n by FINSEQ_1:def_3;
A3: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(DecSD2_(x,n,k))_holds_
(DecSD2_(x,n,k))_._j_=_(DecSD_(x,n,k))_._j
let j be Nat; ::_thesis: ( j in dom (DecSD2 (x,n,k)) implies (DecSD2 (x,n,k)) . j = (DecSD (x,n,k)) . j )
assume A4: j in dom (DecSD2 (x,n,k)) ; ::_thesis: (DecSD2 (x,n,k)) . j = (DecSD (x,n,k)) . j
then (DecSD2 (x,n,k)) . j = DigitDC2 (x,j,k) by A2, Def5
.= DigitDC (x,j,k) by RADIX_1:def_8
.= DigA ((DecSD (x,n,k)),j) by A2, A4, RADIX_1:def_9
.= (DecSD (x,n,k)) . j by A2, A4, RADIX_1:def_3 ;
hence  (DecSD2 (x,n,k)) . j = (DecSD (x,n,k)) . j ; ::_thesis: verum
end;
 len (DecSD (x,n,k)) = n by CARD_1:def_7;
hence  DecSD2 (x,n,k) = DecSD (x,n,k) by A1, A3, FINSEQ_2:9; ::_thesis: verum
end;

theorem Th15: :: RADIX_2:15
for n being Nat st n >= 1 holds
for m, k being Nat st m is_represented_by n,k holds
m = SDDec2 ((DecSD2 (m,n,k)),k)
proof
let n be Nat; ::_thesis: ( n >= 1 implies for m, k being Nat st m is_represented_by n,k holds
m = SDDec2 ((DecSD2 (m,n,k)),k) )
assume A1: n >= 1 ; ::_thesis: for m, k being Nat st m is_represented_by n,k holds
m = SDDec2 ((DecSD2 (m,n,k)),k)
let m, k be Nat; ::_thesis: ( m is_represented_by n,k implies m = SDDec2 ((DecSD2 (m,n,k)),k) )
assume A2: m is_represented_by n,k ; ::_thesis: m = SDDec2 ((DecSD2 (m,n,k)),k)
 SDDec2 ((DecSD2 (m,n,k)),k) = SDDec (DecSD (m,n,k)) by Th13, Th14;
hence  m = SDDec2 ((DecSD2 (m,n,k)),k) by A1, A2, RADIX_1:22; ::_thesis: verum
end;

begin

definition
let q be Integer;
let f, j, k, n be Nat;
let c be Tuple of n,k -SD ;
func Table1 (q,c,f,j) ->  Integer equals :: RADIX_2:def 6
(q * (DigA (c,j))) mod f;
correctness
coherence
(q * (DigA (c,j))) mod f is Integer;
;
end;

:: deftheorem  defines Table1 RADIX_2:def_6_:_
 for q being Integer
for f, j, k, n being Nat
for c being Tuple of n,k -SD holds Table1 (q,c,f,j) = (q * (DigA (c,j))) mod f;

definition
let q be Integer;
let k, f, n be Nat;
let c be Tuple of n,k -SD ;
assume A1: n >= 1 ;
func Mul_mod (q,c,f,k) ->  Tuple of n, INT  means :Def7: :: RADIX_2:def 7
( it . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = it . i & I2 = it . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) );
existence
 ex b1 being Tuple of n, INT st
( b1 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b1 . i & I2 = b1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) )
proof
defpred S1[ Element of NAT , set , set ] means  ex i1, i2 being Integer st
( i1 = $2 & i2 = $3 & i2 = (((Radix k) * i1) + (Table1 (q,c,f,(n -' $1)))) mod f );
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
reconsider T = Table1 (q,c,f,n) as Element of INT by INT_1:def_2;
A2: for i being Element of NAT st 1 <= i & i < n1 holds
for x being Element of INT ex y being Element of INT st S1[i,x,y]
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < n1 implies for x being Element of INT ex y being Element of INT st S1[i,x,y] )
assume that
 1 <= i and
 i < n1 ; ::_thesis: for x being Element of INT ex y being Element of INT st S1[i,x,y]
let x be Element of INT ; ::_thesis: ex y being Element of INT st S1[i,x,y]
reconsider x = x as Integer ;
consider y being Integer such that
A3: y = (((Radix k) * x) + (Table1 (q,c,f,(n -' i)))) mod f ;
reconsider z = y as Element of INT by INT_1:def_2;
take  z ; ::_thesis: S1[i,x,z]
thus  S1[i,x,z] by A3; ::_thesis: verum
end;
consider r being FinSequence of INT  such that
A4: ( len r = n1 & ( r . 1 = T or n1 = 0 ) ) and
A5: for i being Element of NAT st 1 <= i & i < n1 holds
S1[i,r . i,r . (i + 1)] from RECDEF_1:sch_4(A2);
reconsider r = r as Tuple of n, INT by A4, CARD_1:def_7;
take  r ; ::_thesis: ( r . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = r . i & I2 = r . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) )
thus  r . 1 = Table1 (q,c,f,n) by A1, A4; ::_thesis: for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = r . i & I2 = r . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f )
let i be Nat; ::_thesis: ( 1 <= i & i <= n - 1 implies ex I1, I2 being Integer st
( I1 = r . i & I2 = r . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) )
assume A6: ( 1 <= i & i <= n - 1 ) ; ::_thesis: ex I1, I2 being Integer st
( I1 = r . i & I2 = r . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f )
 i in NAT by ORDINAL1:def_12;
hence  ex I1, I2 being Integer st
( I1 = r . i & I2 = r . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) by A5, A6, XREAL_1:147; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Tuple of n, INT st b1 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b1 . i & I2 = b1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) & b2 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b2 . i & I2 = b2 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) holds
b1 = b2
proof
let s1, s2 be Tuple of n, INT ; ::_thesis: ( s1 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = s1 . i & I2 = s1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) & s2 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = s2 . i & I2 = s2 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) implies s1 = s2 )
assume that
A7: s1 . 1 = Table1 (q,c,f,n) and
A8: for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = s1 . i & I2 = s1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) and
A9: s2 . 1 = Table1 (q,c,f,n) and
A10: for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = s2 . i & I2 = s2 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ; ::_thesis: s1 = s2
defpred S1[ Nat] means ( 1 <= $1 & $1 <= n - 1 implies s1 . $1 = s2 . $1 );
A11: for k being Nat st S1[k] holds
S1[k + 1]
proof
let kk be Nat; ::_thesis: ( S1[kk] implies S1[kk + 1] )
assume A12: ( 1 <= kk & kk <= n - 1 implies s1 . kk = s2 . kk ) ; ::_thesis: S1[kk + 1]
A13: ( 0 = kk or ( 0 < kk & 0 + 1 = 1 ) ) ;
assume that
 1 <= kk + 1 and
A14: kk + 1 <= n - 1 ; ::_thesis: s1 . (kk + 1) = s2 . (kk + 1)
percases ( 0 = kk or 1 <= kk ) by A13, NAT_1:13;
suppose 0 = kk ; ::_thesis: s1 . (kk + 1) = s2 . (kk + 1)
hence  s1 . (kk + 1) = s2 . (kk + 1) by A7, A9; ::_thesis: verum
end;
supposeA15: 1 <= kk ; ::_thesis: s1 . (kk + 1) = s2 . (kk + 1)
A16: kk <= kk + 1 by NAT_1:11;
then  kk <= n - 1 by A14, XXREAL_0:2;
then  ( ex I1, I2 being Integer st
( I1 = s1 . kk & I2 = s1 . (kk + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' kk)))) mod f ) & ex i1, i2 being Integer st
( i1 = s2 . kk & i2 = s2 . (kk + 1) & i2 = (((Radix k) * i1) + (Table1 (q,c,f,(n -' kk)))) mod f ) ) by A8, A10, A15;
hence  s1 . (kk + 1) = s2 . (kk + 1) by A12, A14, A15, A16, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A17: len s1 = n by CARD_1:def_7;
A18: S1[ 0 ] ;
A19: for kk being Nat holds S1[kk] from NAT_1:sch_2(A18, A11);
A20: s1 . n = s2 . n
proof
 n - 1 >= 1 - 1 by A1, XREAL_1:9;
then reconsider U1 = n - 1 as Element of NAT by INT_1:3;
now__::_thesis:_s1_._n_=_s2_._n
percases ( U1 = 0 or 0 < U1 ) ;
suppose U1 = 0 ; ::_thesis: s1 . n = s2 . n
hence  s1 . n = s2 . n by A7, A9; ::_thesis: verum
end;
suppose 0 < U1 ; ::_thesis: s1 . n = s2 . n
then A21: 1 <= U1 by NAT_1:14;
then  ( ex i1, i2 being Integer st
( i1 = s1 . U1 & i2 = s1 . (U1 + 1) & i2 = (((Radix k) * i1) + (Table1 (q,c,f,(n -' U1)))) mod f ) & ex j1, j2 being Integer st
( j1 = s2 . U1 & j2 = s2 . (U1 + 1) & j2 = (((Radix k) * j1) + (Table1 (q,c,f,(n -' U1)))) mod f ) ) by A8, A10;
hence  s1 . n = s2 . n by A19, A21; ::_thesis: verum
end;
end;
end;
hence  s1 . n = s2 . n ; ::_thesis: verum
end;
A22: for kk being Nat st 1 <= kk & kk <= len s1 holds
s1 . kk = s2 . kk
proof
let kk be Nat; ::_thesis: ( 1 <= kk & kk <= len s1 implies s1 . kk = s2 . kk )
assume that
A23: 1 <= kk and
A24: kk <= len s1 ; ::_thesis: s1 . kk = s2 . kk
now__::_thesis:_s1_._kk_=_s2_._kk
percases ( kk < len s1 or kk = len s1 ) by A24, XXREAL_0:1;
supposeA25: kk < len s1 ; ::_thesis: s1 . kk = s2 . kk
 n - 1 >= 1 - 1 by A1, XREAL_1:9;
then reconsider U1 = (len s1) - 1 as Element of NAT by A17, INT_1:3;
 U1 + 1 = len s1 ;
then  kk <= U1 by A25, NAT_1:13;
hence  s1 . kk = s2 . kk by A17, A19, A23; ::_thesis: verum
end;
suppose kk = len s1 ; ::_thesis: s1 . kk = s2 . kk
hence  s1 . kk = s2 . kk by A17, A20; ::_thesis: verum
end;
end;
end;
hence  s1 . kk = s2 . kk ; ::_thesis: verum
end;
 len s1 = len s2 by A17, CARD_1:def_7;
hence  s1 = s2 by A22, FINSEQ_1:14; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Mul_mod RADIX_2:def_7_:_
 for q being Integer
for k, f, n being Nat
for c being Tuple of n,k -SD st n >= 1 holds
for b6 being Tuple of n, INT holds
( b6 = Mul_mod (q,c,f,k) iff ( b6 . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b6 . i & I2 = b6 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) ) );

theorem :: RADIX_2:16
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
proof
defpred S1[ 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 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A2: n >= 1 and
A3: S1[n] ; ::_thesis: S1[n + 1]
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 that
A4: ic is_represented_by n + 1,k and
A5: 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 )
deffunc H1( 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 = H1(i) from FINSEQ_2:sch_1();
A8: dom cn = Seg n by A6, 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
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: 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 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 H2( 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 = H2(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: (Mul_mod (q,c,f,k)) . (n + 1) = (q * ic) mod f
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: ( 1 <= i & i <= len cn implies cn . i = cn2 . i )
assume  ( 1 <= i & i <= len cn ) ; ::_thesis: cn . i = cn2 . i
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: verum
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 H3( 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 = H3(i) from FINSEQ_2:sch_1();
reconsider rD = rD as Tuple of n, REAL by A28, CARD_1:def_7;
A30: 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;
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:13
.= n by CARD_1:def_7 ;
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:22
.= n + 1 by A32, CARD_1:def_7 ;
A34: len (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) = n + 1 by CARD_1:def_7;
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: ( 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 that
A36: 1 <= i and
A37: 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
A38: i <= n + 1 by A37, CARD_1:def_7;
then A39: i in Seg (n + 1) by A36, FINSEQ_1:1;
then A40: i in dom (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) by A34, FINSEQ_1:def_3;
percases ( i = 1 or i <> 1 ) ;
supposeA41: 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:41
.= (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) /. 1 by A24, Def2
.= (DigitSD2 ((DecSD2 (ic,(n + 1),k)),k)) . 1 by A40, A41, 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 A41; ::_thesis: verum
end;
supposeA42: 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
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:9;
then reconsider i1 = i - 1 as Element of NAT by INT_1:3;
 1 < i by A36, A42, XXREAL_0:1;
then  1 + 1 <= i by INT_1:7;
then A43: (1 + 1) - 1 <= i - 1 by XREAL_1:9;
 i - 1 <= (n + 1) - 1 by A38, XREAL_1:9;
then A44: i1 in Seg n by A43, FINSEQ_1:1;
 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:24
.= (r2 * rD) . (i - 1) by A29, A30, A31, FINSEQ_1:13
.= r2 * rs by RVSUM_1:45
.= (Radix k) * rs2 by A29, A30, A31, FINSEQ_1:13
.= (Radix k) * ((DigitSD2 (cn2,k)) /. i1) by A30, A44, PARTFUN1:def_6
.= (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:6
.= ((Radix k) |^ i1) * (cn2 . i1) by A43, XREAL_1:235
.= ((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:233
.= (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_6; ::_thesis: verum
end;
end;
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, CARD_1:def_7;
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: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 A45, RVSUM_1:76
.= (SubDigit2 ((DecSD2 (ic,(n + 1),k)),1,k)) + (Sum (r2 * rD)) by A29, A30, A31, 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 A29, A30, A31, 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: verum
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 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 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:14;
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:232
.= (ic mod ((Radix k) |^ 1)) div 1 by NEWTON:4
.= ic mod ((Radix k) |^ 1) by NAT_2:4
.= ic mod (Radix k) by NEWTON:5 ;
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_9
.= [\((((DecSD2 (ic,(n + 1),k)) . 1) / (Radix k)) + (SDDec2 (cn2,k)))/] by A50, 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, A49, NAT_D:1, NAT_D:27 ;
A52: Radix k <> 0 by Th6;
let i be Nat; ::_thesis: ( 1 <= i & i <= len cn implies cn . i = (DecSD2 ((SDDec2 (cn2,k)),n,k)) . i )
assume that
A53: 1 <= i and
A54: i <= len cn ; ::_thesis: cn . i = (DecSD2 ((SDDec2 (cn2,k)),n,k)) . i
A55: i in Seg n by A6, A53, A54, FINSEQ_1:1;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
A56: 1 <= i + 1 by A53, XREAL_1:29;
 ( 1 <= i + 1 & i + 1 <= n + 1 ) by A6, A53, A54, XREAL_1:6, XREAL_1:29;
then A57: i + 1 in Seg (n + 1) by FINSEQ_1:1;
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:26
.= ((SDDec2 (cn2,k)) div ((Radix k) |^ (i -' 1))) mod (Radix k) by A51, NAT_2:27
.= DigitDC2 ((SDDec2 (cn2,k)),i,k) by A53, Th4, Th6 ;
hence  cn . i = (DecSD2 ((SDDec2 (cn2,k)),n,k)) . i by A55, Def5; ::_thesis: verum
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 A48, FINSEQ_1:14;
then A58: 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 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: ( i in Seg n implies DigA (cn,i) = DigA (c,(i + 1)) )
assume A61: 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 A7, A8, A61 ;
hence  DigA (cn,i) = DigA (c,(i + 1)) by A61, RADIX_1:def_3; ::_thesis: verum
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 S2[ 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 S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] )
assume A64: ( i in Seg n implies (Mul_mod (q,cn,f,k)) . i = (Mul_mod (q,c,f,k)) . i ) ; ::_thesis: S2[i + 1]
A65: ( i = 0 or i + 1 > 1 + 0 ) by XREAL_1:6;
assume  i + 1 in Seg n ; ::_thesis: (Mul_mod (q,cn,f,k)) . (i + 1) = (Mul_mod (q,c,f,k)) . (i + 1)
then A66: i + 1 <= n by FINSEQ_1:1;
then A67: (i + 1) - 1 <= n - 1 by XREAL_1:9;
A68: n in Seg n by A2, FINSEQ_1:1;
now__::_thesis:_(_(_i_=_0_&_(Mul_mod_(q,cn,f,k))_._(i_+_1)_=_(Mul_mod_(q,c,f,k))_._(i_+_1)_)_or_(_i_>=_1_&_(Mul_mod_(q,cn,f,k))_._(i_+_1)_=_(Mul_mod_(q,c,f,k))_._(i_+_1)_)_)
percases ( i = 0 or i >= 1 ) by A65, NAT_1:13;
caseA69: 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 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: verum
end;
caseA70: 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 A2, INT_1:5;
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:9;
then  1 <= n -' i by A71, XREAL_1:233;
then A74: n -' i in Seg n by A73, 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, 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:1
.= (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: verum
end;
end;
end;
hence  (Mul_mod (q,cn,f,k)) . (i + 1) = (Mul_mod (q,c,f,k)) . (i + 1) ; ::_thesis: verum
end;
A75: S2[ 0 ] by FINSEQ_1:1;
 for i being Element of NAT holds S2[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: verum
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: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 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: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 A46; ::_thesis: verum
end;
A77: S1[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 that
A78: ic is_represented_by 1,k and
 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 A79: 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 A79, Th7 ;
hence  (Mul_mod (q,c,f,k)) . 1 = (q * ic) mod f by A78, RADIX_1:22; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[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: verum
end;

begin

definition
let n, f, j, m be Nat;
let e be Tuple of n, NAT ;
func Table2 (m,e,f,j) ->  Element of NAT  equals :: RADIX_2:def 8
(m |^ (e /. j)) mod f;
correctness
coherence
(m |^ (e /. j)) mod f is Element of NAT ;
;
end;

:: deftheorem  defines Table2 RADIX_2:def_8_:_
 for n, f, j, m being Nat
for e being Tuple of n, NAT holds Table2 (m,e,f,j) = (m |^ (e /. j)) mod f;

definition
let k, f, m, n be Nat;
let e be Tuple of n, NAT ;
assume A1: n >= 1 ;
func Pow_mod (m,e,f,k) ->  Tuple of n, NAT  means :Def9: :: RADIX_2:def 9
( it . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = it . i & i2 = it . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) );
existence
 ex b1 being Tuple of n, NAT st
( b1 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b1 . i & i2 = b1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) )
proof
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
reconsider T = Table2 (m,e,f,n) as Element of NAT ;
defpred S1[ Nat, set , set ] means  ex i1, i2 being Nat st
( i1 = $2 & i2 = $3 & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n1 -' $1)))) mod f );
A2: for i being Element of NAT st 1 <= i & i < n1 holds
for x being Element of NAT ex y being Element of NAT st S1[i,x,y]
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < n1 implies for x being Element of NAT ex y being Element of NAT st S1[i,x,y] )
assume that
 1 <= i and
 i < n1 ; ::_thesis: for x being Element of NAT ex y being Element of NAT st S1[i,x,y]
let x be Element of NAT ; ::_thesis: ex y being Element of NAT st S1[i,x,y]
reconsider x = x as Element of NAT ;
consider y being Element of NAT  such that
A3: y = (((x |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ;
reconsider z = y as Element of NAT ;
take  z ; ::_thesis: S1[i,x,z]
thus  S1[i,x,z] by A3; ::_thesis: verum
end;
consider r being FinSequence of NAT  such that
A4: ( len r = n1 & ( r . 1 = T or n1 = 0 ) ) and
A5: for i being Element of NAT st 1 <= i & i < n1 holds
S1[i,r . i,r . (i + 1)] from RECDEF_1:sch_4(A2);
reconsider r = r as Tuple of n, NAT by A4, CARD_1:def_7;
take  r ; ::_thesis: ( r . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = r . i & i2 = r . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) )
thus  r . 1 = Table2 (m,e,f,n) by A1, A4; ::_thesis: for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = r . i & i2 = r . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f )
let i be Nat; ::_thesis: ( 1 <= i & i <= n - 1 implies ex i1, i2 being Nat st
( i1 = r . i & i2 = r . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) )
assume A6: ( 1 <= i & i <= n - 1 ) ; ::_thesis: ex i1, i2 being Nat st
( i1 = r . i & i2 = r . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f )
 i in NAT by ORDINAL1:def_12;
hence  ex i1, i2 being Nat st
( i1 = r . i & i2 = r . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) by A5, A6, XREAL_1:147; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Tuple of n, NAT st b1 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b1 . i & i2 = b1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) & b2 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b2 . i & i2 = b2 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) holds
b1 = b2
proof
let s1, s2 be Tuple of n, NAT ; ::_thesis: ( s1 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = s1 . i & i2 = s1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) & s2 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = s2 . i & i2 = s2 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) implies s1 = s2 )
assume that
A7: s1 . 1 = Table2 (m,e,f,n) and
A8: for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Nat st
( I1 = s1 . i & I2 = s1 . (i + 1) & I2 = (((I1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) and
A9: s2 . 1 = Table2 (m,e,f,n) and
A10: for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Nat st
( I1 = s2 . i & I2 = s2 . (i + 1) & I2 = (((I1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ; ::_thesis: s1 = s2
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= n - 1 implies s1 . $1 = s2 . $1 );
A11: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let kk be Element of NAT ; ::_thesis: ( S1[kk] implies S1[kk + 1] )
assume A12: ( 1 <= kk & kk <= n - 1 implies s1 . kk = s2 . kk ) ; ::_thesis: S1[kk + 1]
A13: ( 0 = kk or ( 0 < kk & 0 + 1 = 1 ) ) ;
assume that
 1 <= kk + 1 and
A14: kk + 1 <= n - 1 ; ::_thesis: s1 . (kk + 1) = s2 . (kk + 1)
percases ( 0 = kk or 1 <= kk ) by A13, NAT_1:13;
suppose 0 = kk ; ::_thesis: s1 . (kk + 1) = s2 . (kk + 1)
hence  s1 . (kk + 1) = s2 . (kk + 1) by A7, A9; ::_thesis: verum
end;
supposeA15: 1 <= kk ; ::_thesis: s1 . (kk + 1) = s2 . (kk + 1)
A16: kk <= kk + 1 by NAT_1:11;
then  kk <= n - 1 by A14, XXREAL_0:2;
then  ( ex i1, i2 being Nat st
( i1 = s1 . kk & i2 = s1 . (kk + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' kk)))) mod f ) & ex i1, i2 being Nat st
( i1 = s2 . kk & i2 = s2 . (kk + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' kk)))) mod f ) ) by A8, A10, A15;
hence  s1 . (kk + 1) = s2 . (kk + 1) by A12, A14, A15, A16, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A17: len s1 = n by CARD_1:def_7;
A18: S1[ 0 ] ;
A19: for kk being Element of NAT holds S1[kk] from NAT_1:sch_1(A18, A11);
A20: s1 . n = s2 . n
proof
 n - 1 >= 1 - 1 by A1, XREAL_1:9;
then reconsider U1 = n - 1 as Element of NAT by INT_1:3;
now__::_thesis:_s1_._n_=_s2_._n
percases ( U1 = 0 or 0 < U1 ) ;
suppose U1 = 0 ; ::_thesis: s1 . n = s2 . n
hence  s1 . n = s2 . n by A7, A9; ::_thesis: verum
end;
suppose 0 < U1 ; ::_thesis: s1 . n = s2 . n
then A21: 1 <= U1 by NAT_1:14;
then  ( ex i1, i2 being Nat st
( i1 = s1 . U1 & i2 = s1 . (U1 + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' U1)))) mod f ) & ex j1, j2 being Nat st
( j1 = s2 . U1 & j2 = s2 . (U1 + 1) & j2 = (((j1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' U1)))) mod f ) ) by A8, A10;
hence  s1 . n = s2 . n by A19, A21; ::_thesis: verum
end;
end;
end;
hence  s1 . n = s2 . n ; ::_thesis: verum
end;
A22: for kk being Nat st 1 <= kk & kk <= len s1 holds
s1 . kk = s2 . kk
proof
let kk be Nat; ::_thesis: ( 1 <= kk & kk <= len s1 implies s1 . kk = s2 . kk )
assume that
A23: 1 <= kk and
A24: kk <= len s1 ; ::_thesis: s1 . kk = s2 . kk
A25: kk in NAT by ORDINAL1:def_12;
now__::_thesis:_s1_._kk_=_s2_._kk
percases ( kk < len s1 or kk = len s1 ) by A24, XXREAL_0:1;
supposeA26: kk < len s1 ; ::_thesis: s1 . kk = s2 . kk
 n - 1 >= 1 - 1 by A1, XREAL_1:9;
then reconsider U1 = (len s1) - 1 as Element of NAT by A17, INT_1:3;
 U1 + 1 = len s1 ;
then  kk <= U1 by A26, NAT_1:13;
hence  s1 . kk = s2 . kk by A17, A19, A23, A25; ::_thesis: verum
end;
suppose kk = len s1 ; ::_thesis: s1 . kk = s2 . kk
hence  s1 . kk = s2 . kk by A17, A20; ::_thesis: verum
end;
end;
end;
hence  s1 . kk = s2 . kk ; ::_thesis: verum
end;
 len s1 = len s2 by A17, CARD_1:def_7;
hence  s1 = s2 by A22, FINSEQ_1:14; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines Pow_mod RADIX_2:def_9_:_
 for k, f, m, n being Nat
for e being Tuple of n, NAT st n >= 1 holds
for b6 being Tuple of n, NAT holds
( b6 = Pow_mod (m,e,f,k) iff ( b6 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b6 . i & i2 = b6 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) ) );

theorem :: RADIX_2:17
for n being Nat st n >= 1 holds
for m, k, f, ie being Nat st ie is_represented_by n,k & f > 0 holds
for e being Tuple of n, NAT st e = DecSD2 (ie,n,k) holds
(Pow_mod (m,e,f,k)) . n = (m |^ ie) mod f
proof
defpred S1[ Nat] means  for m, k, f, ie being Nat st ie is_represented_by $1,k & f > 0 holds
for e being Tuple of $1, NAT st e = DecSD2 (ie,$1,k) holds
(Pow_mod (m,e,f,k)) . $1 = (m |^ ie) mod f;
A1: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A2: n >= 1 and
A3: S1[n] ; ::_thesis: S1[n + 1]
let m, k, f, ie be Nat; ::_thesis: ( ie is_represented_by n + 1,k & f > 0 implies for e being Tuple of n + 1, NAT st e = DecSD2 (ie,(n + 1),k) holds
(Pow_mod (m,e,f,k)) . (n + 1) = (m |^ ie) mod f )
A4: n + 1 >= 1 by NAT_1:12;
assume that
A5: ie is_represented_by n + 1,k and
A6: f > 0 ; ::_thesis: for e being Tuple of n + 1, NAT st e = DecSD2 (ie,(n + 1),k) holds
(Pow_mod (m,e,f,k)) . (n + 1) = (m |^ ie) mod f
let e be Tuple of n + 1, NAT ; ::_thesis: ( e = DecSD2 (ie,(n + 1),k) implies (Pow_mod (m,e,f,k)) . (n + 1) = (m |^ ie) mod f )
assume A7: e = DecSD2 (ie,(n + 1),k) ; ::_thesis: (Pow_mod (m,e,f,k)) . (n + 1) = (m |^ ie) mod f
reconsider n = n as Element of NAT by ORDINAL1:def_12;
deffunc H1( Nat) ->  Element of NAT = e . ($1 + 1);
consider en being FinSequence of NAT  such that
A8: len en = n and
A9: for i being Nat st i in dom en holds
en . i = H1(i) from FINSEQ_2:sch_1();
A10: dom en = Seg n by A8, FINSEQ_1:def_3;
reconsider en = en as Tuple of n, NAT by A8, CARD_1:def_7;
A11: n in Seg n by A2, FINSEQ_1:1;
A12: ie < (Radix k) |^ (n + 1) by A5, RADIX_1:def_12;
set ien = SDDec2 (en,k);
A13: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1;
then A14: 1 in Seg (1 + n) by FINSEQ_2:8;
A15: ie = ((SDDec2 (en,k)) * (Radix k)) + (e /. 1)
proof
A16: len <*(SubDigit2 (e,1,k))*> = 1 by FINSEQ_1:39;
deffunc H2( Nat) ->  Element of NAT = (DigitSD2 (en,k)) . $1;
reconsider r2 = Radix k as Element of REAL by XREAL_0:def_1;
consider rD being FinSequence of REAL  such that
A17: len rD = n and
A18: for i being Nat st i in dom rD holds
rD . i = H2(i) from FINSEQ_2:sch_1();
reconsider rD = rD as Tuple of n, REAL by A17, CARD_1:def_7;
A19: dom rD = Seg n by A17, FINSEQ_1:def_3;
reconsider rD1 = rD as Element of n -tuples_on REAL by FINSEQ_2:131;
A20: dom (DigitSD2 (en,k)) = Seg (len (DigitSD2 (en,k))) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
then A21: len ((Radix k) * (DigitSD2 (en,k))) = len (r2 * rD1) by A18, A19, FINSEQ_1:13
.= n by CARD_1:def_7 ;
A22: len (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) = (len <*(SubDigit2 (e,1,k))*>) + (len ((Radix k) * (DigitSD2 (en,k)))) by FINSEQ_1:22
.= n + 1 by A21, CARD_1:def_7 ;
A23: len (DigitSD2 (e,k)) = n + 1 by CARD_1:def_7;
A24: for i being Nat st 1 <= i & i <= len (DigitSD2 (e,k)) holds
(DigitSD2 (e,k)) . i = (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (DigitSD2 (e,k)) implies (DigitSD2 (e,k)) . i = (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) . i )
assume that
A25: 1 <= i and
A26: i <= len (DigitSD2 (e,k)) ; ::_thesis: (DigitSD2 (e,k)) . i = (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) . i
A27: i <= n + 1 by A26, CARD_1:def_7;
then A28: i in Seg (n + 1) by A25, FINSEQ_1:1;
then A29: i in dom (DigitSD2 (e,k)) by A23, FINSEQ_1:def_3;
percases ( i = 1 or i <> 1 ) ;
supposeA30: i = 1 ; ::_thesis: (DigitSD2 (e,k)) . i = (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) . i
then (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) . i = SubDigit2 (e,1,k) by FINSEQ_1:41
.= (DigitSD2 (e,k)) /. 1 by A14, Def2
.= (DigitSD2 (e,k)) . 1 by A29, A30, PARTFUN1:def_6 ;
hence  (DigitSD2 (e,k)) . i = (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) . i by A30; ::_thesis: verum
end;
supposeA31: i <> 1 ; ::_thesis: (DigitSD2 (e,k)) . i = (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) . i
reconsider rs2 = (DigitSD2 (en,k)) . (i - 1) as Element of NAT ;
reconsider rs = rD . (i - 1) as Real ;
 1 - 1 <= i - 1 by A25, XREAL_1:9;
then reconsider i1 = i - 1 as Element of NAT by INT_1:3;
 1 < i by A25, A31, XXREAL_0:1;
then  1 + 1 <= i by INT_1:7;
then A32: (1 + 1) - 1 <= i - 1 by XREAL_1:9;
A33: i - 1 <= (n + 1) - 1 by A27, XREAL_1:9;
then A34: i1 in Seg n by A32, FINSEQ_1:1;
A35: i1 in dom rD by A19, A32, A33, FINSEQ_1:1;
 1 < i by A25, A31, XXREAL_0:1;
then (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) . i = ((Radix k) * (DigitSD2 (en,k))) . (i - 1) by A16, A22, A27, FINSEQ_1:24
.= (r2 * rD) . (i - 1) by A18, A20, A19, FINSEQ_1:13
.= r2 * rs by RVSUM_1:45
.= (Radix k) * rs2 by A18, A20, A19, FINSEQ_1:13
.= (Radix k) * ((DigitSD2 (en,k)) /. i1) by A20, A19, A35, PARTFUN1:def_6
.= (Radix k) * (SubDigit2 (en,i1,k)) by A34, Def2
.= ((Radix k) * ((Radix k) |^ (i1 -' 1))) * (en . i1)
.= ((Radix k) |^ ((i1 -' 1) + 1)) * (en . i1) by NEWTON:6
.= ((Radix k) |^ i1) * (en . i1) by A32, XREAL_1:235
.= ((Radix k) |^ i1) * (e . (i1 + 1)) by A9, A10, A34
.= SubDigit2 (e,i,k) by A25, XREAL_1:233
.= (DigitSD2 (e,k)) /. i by A28, Def2 ;
hence  (DigitSD2 (e,k)) . i = (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) . i by A29, PARTFUN1:def_6; ::_thesis: verum
end;
end;
end;
 len (DigitSD2 (e,k)) = len (<*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k)))) by A22, CARD_1:def_7;
then A36: DigitSD2 (e,k) = <*(SubDigit2 (e,1,k))*> ^ ((Radix k) * (DigitSD2 (en,k))) by A24, FINSEQ_1:14;
 dom e = Seg (len e) by FINSEQ_1:def_3;
then A37: 1 in dom e by A14, CARD_1:def_7;
A38: 1 - 1 = 0 ;
ie = SDDec2 (e,k) by A5, A7, Th15, NAT_1:12
.= (SubDigit2 (e,1,k)) + (Sum ((Radix k) * (DigitSD2 (en,k)))) by A36, RVSUM_1:76
.= (SubDigit2 (e,1,k)) + (Sum (r2 * rD)) by A18, A20, A19, FINSEQ_1:13
.= (SubDigit2 (e,1,k)) + (r2 * (Sum rD)) by RVSUM_1:87
.= (SubDigit2 (e,1,k)) + ((Radix k) * (SDDec2 (en,k))) by A18, A20, A19, FINSEQ_1:13
.= (((Radix k) |^ 0) * (e . 1)) + ((Radix k) * (SDDec2 (en,k))) by A38, XREAL_0:def_2
.= (1 * (e . 1)) + ((Radix k) * (SDDec2 (en,k))) by NEWTON:4 ;
hence  ie = ((SDDec2 (en,k)) * (Radix k)) + (e /. 1) by A37, PARTFUN1:def_6; ::_thesis: verum
end;
then  ie >= (SDDec2 (en,k)) * (Radix k) by INT_1:6;
then  (SDDec2 (en,k)) * (Radix k) < (Radix k) |^ (n + 1) by A12, XXREAL_0:2;
then  (SDDec2 (en,k)) * (Radix k) < ((Radix k) |^ n) * (Radix k) by NEWTON:6;
then  SDDec2 (en,k) < (Radix k) |^ n by XREAL_1:64;
then A39: SDDec2 (en,k) is_represented_by n,k by RADIX_1:def_12;
A40: n + 1 in Seg (n + 1) by A4, FINSEQ_1:1;
A41: for i being Element of NAT st i in Seg n holds
(Pow_mod (m,en,f,k)) . i = (Pow_mod (m,e,f,k)) . i
proof
defpred S2[ Element of NAT ] means ( $1 in Seg n implies (Pow_mod (m,en,f,k)) . $1 = (Pow_mod (m,e,f,k)) . $1 );
A42: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] )
assume A43: ( i in Seg n implies (Pow_mod (m,en,f,k)) . i = (Pow_mod (m,e,f,k)) . i ) ; ::_thesis: S2[i + 1]
A44: ( i = 0 or i + 1 > 1 + 0 ) by XREAL_1:6;
A45: dom en = Seg n by A8, FINSEQ_1:def_3;
assume A46: i + 1 in Seg n ; ::_thesis: (Pow_mod (m,en,f,k)) . (i + 1) = (Pow_mod (m,e,f,k)) . (i + 1)
then A47: i + 1 <= n by FINSEQ_1:1;
then A48: (i + 1) - 1 <= n - 1 by XREAL_1:9;
A49: dom e = Seg (len e) by FINSEQ_1:def_3;
then A50: dom e = Seg (n + 1) by CARD_1:def_7;
now__::_thesis:_(_(_i_=_0_&_(Pow_mod_(m,en,f,k))_._(i_+_1)_=_(Pow_mod_(m,e,f,k))_._(i_+_1)_)_or_(_i_>=_1_&_(Pow_mod_(m,en,f,k))_._(i_+_1)_=_(Pow_mod_(m,e,f,k))_._(i_+_1)_)_)
percases ( i = 0 or i >= 1 ) by A44, NAT_1:13;
caseA51: i = 0 ; ::_thesis: (Pow_mod (m,en,f,k)) . (i + 1) = (Pow_mod (m,e,f,k)) . (i + 1)
then (Pow_mod (m,en,f,k)) . (i + 1) = Table2 (m,en,f,n) by A2, Def9
.= (m |^ (en . n)) mod f by A11, A45, PARTFUN1:def_6
.= (m |^ (e . (n + 1))) mod f by A9, A10, A11
.= Table2 (m,e,f,(n + 1)) by A40, A50, PARTFUN1:def_6
.= (Pow_mod (m,e,f,k)) . 1 by A4, Def9 ;
hence  (Pow_mod (m,en,f,k)) . (i + 1) = (Pow_mod (m,e,f,k)) . (i + 1) by A51; ::_thesis: verum
end;
caseA52: i >= 1 ; ::_thesis: (Pow_mod (m,en,f,k)) . (i + 1) = (Pow_mod (m,e,f,k)) . (i + 1)
reconsider nn = n - 1 as Element of NAT by A2, INT_1:5;
A53: i <= nn + 1 by A48, NAT_1:12;
then  i <= (n + 1) - 1 ;
then A54: ex I1, I2 being Nat st
( I1 = (Pow_mod (m,e,f,k)) . i & I2 = (Pow_mod (m,e,f,k)) . (i + 1) & I2 = (((I1 |^ (Radix k)) mod f) * (Table2 (m,e,f,((n + 1) -' i)))) mod f ) by A4, A52, Def9;
A55: ex I1, I2 being Nat st
( I1 = (Pow_mod (m,en,f,k)) . i & I2 = (Pow_mod (m,en,f,k)) . (i + 1) & I2 = (((I1 |^ (Radix k)) mod f) * (Table2 (m,en,f,(n -' i)))) mod f ) by A2, A48, A52, Def9;
A56: n -' i <= n by NAT_D:35;
 i + 1 <= n by A46, FINSEQ_1:1;
then  (i + 1) - 1 <= n - 1 by XREAL_1:9;
then  (n + 1) -' i >= (n + 1) -' nn by NAT_D:41;
then  (n + 1) -' i >= (n + 1) - (n - 1) by XREAL_0:def_2;
then  ( (n + 1) -' i <= n + 1 & 1 <= (n + 1) -' i ) by NAT_D:35, XXREAL_0:2;
then  (n + 1) -' i in Seg (n + 1) by FINSEQ_1:1;
then A57: (n + 1) -' i in dom e by A49, CARD_1:def_7;
 (1 + i) - i <= n - i by A47, XREAL_1:9;
then  1 <= n -' i by A53, XREAL_1:233;
then A58: n -' i in Seg n by A56, FINSEQ_1:1;
then  n -' i in dom en by A8, FINSEQ_1:def_3;
then (Pow_mod (m,en,f,k)) . (i + 1) = (((((Pow_mod (m,e,f,k)) . i) |^ (Radix k)) mod f) * ((m |^ (en . (n -' i))) mod f)) mod f by A43, A52, A53, A55, FINSEQ_1:1, PARTFUN1:def_6
.= (((((Pow_mod (m,e,f,k)) . i) |^ (Radix k)) mod f) * ((m |^ (e . ((n -' i) + 1))) mod f)) mod f by A9, A10, A58
.= (((((Pow_mod (m,e,f,k)) . i) |^ (Radix k)) mod f) * ((m |^ (e . ((n + 1) -' i))) mod f)) mod f by A53, NAT_D:38
.= (((((Pow_mod (m,e,f,k)) . i) |^ (Radix k)) mod f) * (Table2 (m,e,f,((n + 1) -' i)))) mod f by A57, PARTFUN1:def_6 ;
hence  (Pow_mod (m,en,f,k)) . (i + 1) = (Pow_mod (m,e,f,k)) . (i + 1) by A54; ::_thesis: verum
end;
end;
end;
hence  (Pow_mod (m,en,f,k)) . (i + 1) = (Pow_mod (m,e,f,k)) . (i + 1) ; ::_thesis: verum
end;
A59: S2[ 0 ] by FINSEQ_1:1;
 for i being Element of NAT holds S2[i] from NAT_1:sch_1(A59, A42);
hence  for i being Element of NAT st i in Seg n holds
(Pow_mod (m,en,f,k)) . i = (Pow_mod (m,e,f,k)) . i ; ::_thesis: verum
end;
A60: Radix k > 0 by Th6;
A61: for i being Nat st 1 <= i & i <= len en holds
en . i = (DecSD2 ((SDDec2 (en,k)),n,k)) . i
proof
 dom e = Seg (len e) by FINSEQ_1:def_3;
then A62: dom e = Seg (n + 1) by CARD_1:def_7;
A63: e . 1 = DigitDC2 (ie,1,k) by A7, A14, Def5
.= (ie mod ((Radix k) |^ 1)) div ((Radix k) |^ 0) by XREAL_1:232
.= (ie mod ((Radix k) |^ 1)) div 1 by NEWTON:4
.= ie mod ((Radix k) |^ 1) by NAT_2:4
.= ie mod (Radix k) by NEWTON:5 ;
A64: 0 < Radix k by Th6;
A65: ((e . 1) + ((SDDec2 (en,k)) * (Radix k))) div (Radix k) = [\(((e . 1) + ((SDDec2 (en,k)) * (Radix k))) / (Radix k))/] by INT_1:def_9
.= [\(((e . 1) / (Radix k)) + (SDDec2 (en,k)))/] by A64, XCMPLX_1:113
.= [\((e . 1) / (Radix k))/] + (SDDec2 (en,k)) by INT_1:28
.= ((e . 1) div (Radix k)) + (SDDec2 (en,k)) by INT_1:def_9
.= 0 + (SDDec2 (en,k)) by A60, A63, NAT_D:1, NAT_D:27 ;
A66: Radix k <> 0 by Th6;
let i be Nat; ::_thesis: ( 1 <= i & i <= len en implies en . i = (DecSD2 ((SDDec2 (en,k)),n,k)) . i )
assume that
A67: 1 <= i and
A68: i <= len en ; ::_thesis: en . i = (DecSD2 ((SDDec2 (en,k)),n,k)) . i
A69: 1 <= i + 1 by A67, XREAL_1:29;
 ( 1 <= i + 1 & i + 1 <= n + 1 ) by A8, A67, A68, XREAL_1:6, XREAL_1:29;
then A70: i + 1 in Seg (n + 1) by FINSEQ_1:1;
A71: i in Seg n by A8, A67, A68, FINSEQ_1:1;
then en . i = e . (i + 1) by A9, A10
.= DigitDC2 (ie,(i + 1),k) by A7, A70, Def5
.= ((((SDDec2 (en,k)) * (Radix k)) + (e /. 1)) div ((Radix k) |^ ((i + 1) -' 1))) mod (Radix k) by A15, A69, Th4, Th6
.= ((((SDDec2 (en,k)) * (Radix k)) + (e . 1)) div ((Radix k) |^ ((i + 1) -' 1))) mod (Radix k) by A13, A62, FINSEQ_2:8, PARTFUN1:def_6
.= ((((SDDec2 (en,k)) * (Radix k)) + (e . 1)) div ((Radix k) |^ i)) mod (Radix k) by NAT_D:34
.= ((((SDDec2 (en,k)) * (Radix k)) + (e . 1)) div ((Radix k) * ((Radix k) |^ (i -' 1)))) mod (Radix k) by A67, A66, PEPIN:26
.= ((((e . 1) + ((SDDec2 (en,k)) * (Radix k))) div (Radix k)) div ((Radix k) |^ (i -' 1))) mod (Radix k) by NAT_2:27
.= DigitDC2 ((SDDec2 (en,k)),i,k) by A67, A65, Th4, Th6 ;
hence  en . i = (DecSD2 ((SDDec2 (en,k)),n,k)) . i by A71, Def5; ::_thesis: verum
end;
 len en = len (DecSD2 ((SDDec2 (en,k)),n,k)) by A8, CARD_1:def_7;
then A72: en = DecSD2 ((SDDec2 (en,k)),n,k) by A61, FINSEQ_1:14;
 ( n <= (n + 1) - 1 & n + 1 >= 1 ) by NAT_1:11;
then  ex I1, I2 being Nat st
( I1 = (Pow_mod (m,e,f,k)) . n & I2 = (Pow_mod (m,e,f,k)) . (n + 1) & I2 = (((I1 |^ (Radix k)) mod f) * (Table2 (m,e,f,((n + 1) -' n)))) mod f ) by A2, Def9;
then (Pow_mod (m,e,f,k)) . (n + 1) = (((((Pow_mod (m,en,f,k)) . n) |^ (Radix k)) mod f) * (Table2 (m,e,f,((n + 1) -' n)))) mod f by A2, A41, FINSEQ_1:3
.= (((((m |^ (SDDec2 (en,k))) mod f) |^ (Radix k)) mod f) * (Table2 (m,e,f,((n + 1) -' n)))) mod f by A3, A6, A39, A72
.= ((((m |^ (SDDec2 (en,k))) |^ (Radix k)) mod f) * (Table2 (m,e,f,((n + 1) -' n)))) mod f by PEPIN:12
.= (((m |^ (SDDec2 (en,k))) |^ (Radix k)) * (Table2 (m,e,f,((n + 1) -' n)))) mod f by EULER_2:8
.= ((m |^ ((SDDec2 (en,k)) * (Radix k))) * (Table2 (m,e,f,((n + 1) -' n)))) mod f by NEWTON:9
.= ((m |^ ((SDDec2 (en,k)) * (Radix k))) * ((m |^ (e /. 1)) mod f)) mod f by NAT_D:34
.= ((m |^ ((SDDec2 (en,k)) * (Radix k))) * (m |^ (e /. 1))) mod f by EULER_2:7
.= (m |^ (((SDDec2 (en,k)) * (Radix k)) + (e /. 1))) mod f by NEWTON:8 ;
hence  (Pow_mod (m,e,f,k)) . (n + 1) = (m |^ ie) mod f by A15; ::_thesis: verum
end;
A73: S1[1]
proof
let m, k, f, ie be Nat; ::_thesis: ( ie is_represented_by 1,k & f > 0 implies for e being Tuple of 1, NAT st e = DecSD2 (ie,1,k) holds
(Pow_mod (m,e,f,k)) . 1 = (m |^ ie) mod f )
assume that
A74: ie is_represented_by 1,k and
 f > 0 ; ::_thesis: for e being Tuple of 1, NAT st e = DecSD2 (ie,1,k) holds
(Pow_mod (m,e,f,k)) . 1 = (m |^ ie) mod f
 ie < (Radix k) |^ 1 by A74, RADIX_1:def_12;
then A75: ie < Radix k by NEWTON:5;
let e be Tuple of 1, NAT ; ::_thesis: ( e = DecSD2 (ie,1,k) implies (Pow_mod (m,e,f,k)) . 1 = (m |^ ie) mod f )
A76: 1 - 1 = 0 ;
A77: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1;
 len (DecSD2 (ie,1,k)) = 1 by CARD_1:def_7;
then A78: 1 in dom (DecSD2 (ie,1,k)) by A77, FINSEQ_1:def_3;
assume  e = DecSD2 (ie,1,k) ; ::_thesis: (Pow_mod (m,e,f,k)) . 1 = (m |^ ie) mod f
then e /. 1 = (DecSD2 (ie,1,k)) . 1 by A78, PARTFUN1:def_6
.= DigitDC2 (ie,1,k) by A77, Def5
.= (ie mod ((Radix k) |^ 1)) div ((Radix k) |^ 0) by A76, XREAL_0:def_2
.= (ie mod ((Radix k) |^ 1)) div 1 by NEWTON:4
.= ie mod ((Radix k) |^ 1) by NAT_2:4
.= ie mod (Radix k) by NEWTON:5
.= ie by A75, NAT_D:24 ;
then  (m |^ ie) mod f = Table2 (m,e,f,1) ;
hence  (Pow_mod (m,e,f,k)) . 1 = (m |^ ie) mod f by Def9; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A73, A1);
hence  for n being Nat st n >= 1 holds
for m, k, f, ie being Nat st ie is_represented_by n,k & f > 0 holds
for e being Tuple of n, NAT st e = DecSD2 (ie,n,k) holds
(Pow_mod (m,e,f,k)) . n = (m |^ ie) mod f ; ::_thesis: verum
end;