defpred S1[ Nat] means P1[F1() + $1];
consider i1 being Integer such that
A3:
P1[i1]
by A2;
ex k being Nat st F1() + k = i1
by A1, A3, Lm5;
then A4:
ex k being Nat st S1[k]
by A3;
consider l being Nat such that
A5:
( S1[l] & ( for n being Nat st S1[n] holds
l <= n ) )
from NAT_1:sch 5(A4);
take i0 = F1() + l; ( P1[i0] & ( for i1 being Integer st P1[i1] holds
i0 <= i1 ) )
for i1 being Integer st P1[i1] holds
i0 <= i1
hence
( P1[i0] & ( for i1 being Integer st P1[i1] holds
i0 <= i1 ) )
by A5; verum