A4:
for x being object st x in F1() /\ F2() holds
ex y being object st
( y in NAT & P1[x,y] )
consider f being Function such that
A7:
( dom f = F1() /\ F2() & rng f c= NAT )
and
A8:
for x being object st x in F1() /\ F2() holds
P1[x,f . x]
from FUNCT_1:sch 6(A4);
reconsider Z = rng f as finite Subset of NAT by A1, A7, FINSET_1:8;
consider n being Nat such that
A9:
for i being Nat st i in Z holds
i <= n
by STIRL2_1:56;
take
n
; for x being Element of F1() st x in F2() holds
P1[x,n]
let x be Element of F1(); ( x in F2() implies P1[x,n] )
assume
x in F2()
; P1[x,n]
then A10:
x in F1() /\ F2()
by XBOOLE_0:def 4;
then A11:
f . x in rng f
by A7, FUNCT_1:def 3;
then reconsider i = f . x as Element of NAT by A7;
i <= n
by A9, A11;
hence
P1[x,n]
by A3, A8, A10; verum