defpred S1[ 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 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
Nat;
( 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
;
for x being Element of INT ex y being Element of INT st S1[i,x,y]
let x be
Element of
INT ;
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
;
S1[i,x,z]
thus
S1[
i,
x,
z]
by A3;
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 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
; ( 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; 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; ( 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 )
; 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
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; verum