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 |^ ()) mod f) * (Table2 (m,e,f,(n1 -' \$1)))) mod f );
A2: for i being 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 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 |^ ()) 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 Nat st 1 <= i & i < n1 holds
S1[i,r . i,r . (i + 1)] from reconsider r = r as Tuple of n, NAT by ;
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 |^ ()) 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 |^ ()) 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 |^ ()) 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 |^ ()) mod f) * (Table2 (m,e,f,(n -' i)))) mod f )

thus ex i1, i2 being Nat st
( i1 = r . i & i2 = r . (i + 1) & i2 = (((i1 |^ ()) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) by ; :: thesis: verum