set A = { [m,n] where m, n is Nat : ( m < F₁() & n < F₂() & P₁[m,n] ) } ;
{ [m,n] where m, n is Nat : ( m < F₁() & n < F₂() & P₁[m,n] ) } c= [:F₁(),F₂():]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [m,n] where m, n is Nat : ( m < F₁() & n < F₂() & P₁[m,n] ) } or a in [:F₁(),F₂():] )
assume a in { [m,n] where m, n is Nat : ( m < F₁() & n < F₂() & P₁[m,n] ) } ; :: thesis: a in [:F₁(),F₂():]
then consider m, n being Nat such that
A1: a = [m,n] and
A2: ( m < F₁() & n < F₂() ) and
P₁[m,n] ;
( m in Segm F₁() & n in Segm F₂() ) by A2, NAT_1:44;
hence a in [:F₁(),F₂():] by A1, ZFMISC_1:def 2; :: thesis: verum

end;

hence { [m,n] where m, n is Nat : ( m < F₁() & n < F₂() & P₁[m,n] ) } is finite ; :: thesis: verum