defpred S_{1}[ 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 S_{1}[i,x,y]

A4: ( len r = n1 & ( r . 1 = T or n1 = 0 ) ) and

A5: for i being Nat st 1 <= i & i < n1 holds

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

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

( 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 S

proof

consider r being FinSequence of INT such that
let i be Nat; :: thesis: ( 1 <= i & i < n1 implies for x being Element of INT ex y being Element of INT st S_{1}[i,x,y] )

assume that

1 <= i and

i < n1 ; :: thesis: for x being Element of INT ex y being Element of INT st S_{1}[i,x,y]

let x be Element of INT ; :: thesis: ex y being Element of INT st S_{1}[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: S_{1}[i,x,z]

thus S_{1}[i,x,z]
by A3; :: thesis: verum

end;assume that

1 <= i and

i < n1 ; :: thesis: for x being Element of INT ex y being Element of INT st S

let x be Element of INT ; :: thesis: ex y being Element of INT st S

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

thus S

A4: ( len r = n1 & ( r . 1 = T or n1 = 0 ) ) and

A5: for i being Nat st 1 <= i & i < n1 holds

S

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 )

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