reconsider T = Table2 m,e,f,n as Element of NAT ;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
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
( 1
<= i &
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, FINSEQ_2:110;
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 ) )
A6:
i in NAT
by ORDINAL1:def 13;
assume
( 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 )
then
( 1 <= i & i < n )
by XREAL_1:149;
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; :: thesis: verum