A4: for x being object st x in F1() /\ F2() holds
ex y being object st
( y in NAT & P1[x,y] )
proof
let x be object ; :: thesis: ( x in F1() /\ F2() implies ex y being object st
( y in NAT & P1[x,y] ) )
assume A5: x in F1() /\ F2() ; :: thesis: ex y being object st
( y in NAT & P1[x,y] )
then reconsider x = x as Element of F1() by XBOOLE_0:def 4;
x in F2() by A5, XBOOLE_0:def 4;
then consider n being Nat such that
A6: P1[x,n] by A2;
n is Element of NAT by ORDINAL1:def 12;
hence ex y being object st
( y in NAT & P1[x,y] ) by A6; :: thesis: verum
end;
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 ; :: thesis: for x being Element of F1() st x in F2() holds
P1[x,n]
let x be Element of F1(); :: thesis: ( x in F2() implies P1[x,n] )
assume x in F2() ; :: thesis: 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; :: thesis: verum