A4: for x being object st x in F₁() /\ F₂() holds
ex y being object st
( y in NAT & P₁[x,y] )

proof

let x be object ; :: thesis: ( x in F₁() /\ F₂() implies ex y being object st
( y in NAT & P₁[x,y] ) )
assume A5: x in F₁() /\ F₂() ; :: thesis: ex y being object st
( y in NAT & P₁[x,y] )
then reconsider x = x as Element of F₁() by XBOOLE_0:def 4;
x in F₂() by A5, XBOOLE_0:def 4;
then consider n being Nat such that
A6: P₁[x,n] by A2;
n is Element of NAT by ORDINAL1:def 12;
hence ex y being object st
( y in NAT & P₁[x,y] ) by A6; :: thesis: verum

end;

consider f being Function such that
A7: ( dom f = F₁() /\ F₂() & rng f c= NAT ) and
A8: for x being object st x in F₁() /\ F₂() holds
P₁[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 F₁() st x in F₂() holds
P₁[x,n]
let x be Element of F₁(); :: thesis: ( x in F₂() implies P₁[x,n] )
assume x in F₂() ; :: thesis: P₁[x,n]
then A10: x in F₁() /\ F₂() 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 P₁[x,n] by A3, A8, A10; :: thesis: verum