defpred S_{1}[ 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_{1}[n] holds

S_{1}[n + 1]
_{1}[1]

S_{1}[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: verum

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

S

proof

A78:
S
let n be Nat; :: thesis: ( n >= 1 & S_{1}[n] implies S_{1}[n + 1] )

assume that

A2: n >= 1 and

A3: S_{1}[n]
; :: thesis: S_{1}[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 H_{1}( 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_{1}(i)
from FINSEQ_2:sch 1();

A8: dom cn = Seg n by A6, FINSEQ_1:def 3;

rng cn c= k -SD

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_{2}( 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_{2}(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

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)

.= ((((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

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))

(Mul_mod (q,cn,f,k)) . i = (Mul_mod (q,c,f,k)) . i

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: verum

end;assume that

A2: n >= 1 and

A3: S

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 H

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

A8: dom cn = Seg n by A6, FINSEQ_1:def 3;

rng cn c= k -SD

proof

then reconsider cn = cn as FinSequence of k -SD by FINSEQ_1:def 4;
let z be object ; :: 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 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: verum

end;assume z in rng cn ; :: thesis: z in k -SD

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: verum

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

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

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

then A23:
SDDec cn = SDDec2 (cn2,k)
by A6, A14, Th13, FINSEQ_1:14;
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;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

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

then A47: (q * ic) mod f =
(((q * (Radix k)) * (SDDec2 (cn2,k))) + (q * ((DecSD2 (ic,(n + 1),k)) . 1))) mod f
A26:
len <*(SubDigit2 ((DecSD2 (ic,(n + 1),k)),1,k))*> = 1
by FINSEQ_1:39;

A27: 1 - 1 = 0 ;

deffunc H_{3}( 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_{3}(i)
from FINSEQ_2:sch 1();

A30: for i being Nat st i in dom rD holds

rD . i = (DigitSD2 (cn2,k)) . i

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

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: verum

end;A27: 1 - 1 = 0 ;

deffunc H

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

A30: for i being Nat st i in dom rD holds

rD . i = (DigitSD2 (cn2,k)) . i

proof

reconsider rD = rD as Tuple of n, REAL by A28, CARD_1:def 7;
let i be Nat; :: thesis: ( i in dom rD implies rD . i = (DigitSD2 (cn2,k)) . i )

assume i in dom rD ; :: thesis: rD . i = (DigitSD2 (cn2,k)) . i

then rD . i = H_{3}(i)
by A29;

hence rD . i = (DigitSD2 (cn2,k)) . i ; :: thesis: verum

end;assume i in dom rD ; :: thesis: rD . i = (DigitSD2 (cn2,k)) . i

then rD . i = H

hence rD . i = (DigitSD2 (cn2,k)) . i ; :: thesis: verum

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

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;
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

A37: 1 <= i and

A38: 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

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;

end;assume that

A37: 1 <= i and

A38: 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

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
( i = 1 or i <> 1 )
;

end;

suppose A42:
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 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: verum

end;.= (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: verum

suppose A43:
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 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: verum

end;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: verum

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: verum

.= ((((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

reconsider icn = SDDec cn as Element of NAT by A23;
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: ( 1 <= i & i <= len cn implies cn . i = (DecSD2 ((SDDec2 (cn2,k)),n,k)) . i )

assume that

A54: 1 <= i and

A55: i <= len cn ; :: thesis: cn . i = (DecSD2 ((SDDec2 (cn2,k)),n,k)) . i

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: verum

end;.= (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: ( 1 <= i & i <= len cn implies cn . i = (DecSD2 ((SDDec2 (cn2,k)),n,k)) . i )

assume that

A54: 1 <= i and

A55: i <= len cn ; :: thesis: cn . i = (DecSD2 ((SDDec2 (cn2,k)),n,k)) . i

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: verum

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

A63:
for i being Element of NAT st i in Seg n holds
let i be Element of NAT ; :: thesis: ( i in Seg n implies DigA (cn,i) = DigA (c,(i + 1)) )

assume A62: 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, A62 ;

hence DigA (cn,i) = DigA (c,(i + 1)) by A62, RADIX_1:def 3; :: thesis: verum

end;assume A62: 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, A62 ;

hence DigA (cn,i) = DigA (c,(i + 1)) by A62, RADIX_1:def 3; :: thesis: verum

(Mul_mod (q,cn,f,k)) . i = (Mul_mod (q,c,f,k)) . i

proof

( n <= (n + 1) - 1 & n + 1 >= 1 )
by NAT_1:11;
defpred S_{2}[ 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_{2}[i] holds

S_{2}[i + 1]
_{2}[ 0 ]
by FINSEQ_1:1;

for i being Nat holds S_{2}[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: verum

end;A64: for i being Nat st S

S

proof

A76:
S
let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume A65: ( i in Seg n implies (Mul_mod (q,cn,f,k)) . i = (Mul_mod (q,c,f,k)) . i ) ; :: thesis: S_{2}[i + 1]

A66: ( 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 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;

end;assume A65: ( i in Seg n implies (Mul_mod (q,cn,f,k)) . i = (Mul_mod (q,c,f,k)) . i ) ; :: thesis: S

A66: ( 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 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: ( ( 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) ) )end;

hence
(Mul_mod (q,cn,f,k)) . (i + 1) = (Mul_mod (q,c,f,k)) . (i + 1)
; :: thesis: verumper cases
( i = 0 or i >= 1 )
by A66, NAT_1:13;

end;

case A70:
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 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: verum

end;.= 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: verum

case A71:
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;

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: verum

end;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: verum

for i being Nat holds S

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

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: verum

proof

for n being Nat st n >= 1 holds
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

A79: 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 A80: 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 A80, Th7 ;

hence (Mul_mod (q,c,f,k)) . 1 = (q * ic) mod f by A79, RADIX_1:22; :: thesis: verum

end;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

A79: 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 A80: 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 A80, Th7 ;

hence (Mul_mod (q,c,f,k)) . 1 = (q * ic) mod f by A79, RADIX_1:22; :: thesis: verum

S

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