set F = { f where f is Function of F₁(),F₂() : P₁[f] } ;

now

per cases ( F₂() = 0 or F₂() > 0 ) ;

suppose A1: F₂() = 0 ; :: thesis: { f where f is Function of F₁(),F₂() : P₁[f] } is finite

{ f where f is Function of F₁(),F₂() : P₁[f] } c= {{} }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F₁(),F₂() : P₁[f] } or x in {{} } )
assume A2: x in { f where f is Function of F₁(),F₂() : P₁[f] } ; :: thesis: x in {{} }
consider f being Function of F₁(),F₂() such that
A3: ( x = f & P₁[f] ) by A2;
rng f = {} by A1;
then f = {} ;
hence x in {{} } by A3, TARSKI:def 1; :: thesis: verum

end;

hence { f where f is Function of F₁(),F₂() : P₁[f] } is finite ; :: thesis: verum

end;

suppose A4: F₂() > 0 ; :: thesis: { f where f is Function of F₁(),F₂() : P₁[f] } is finite

A5: { f where f is Function of F₁(),F₂() : P₁[f] } c= Funcs F₁(),F₂()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F₁(),F₂() : P₁[f] } or x in Funcs F₁(),F₂() )
assume A6: x in { f where f is Function of F₁(),F₂() : P₁[f] } ; :: thesis: x in Funcs F₁(),F₂()
ex f being Function of F₁(),F₂() st
( x = f & P₁[f] ) by A6;
hence x in Funcs F₁(),F₂() by A4, FUNCT_2:11; :: thesis: verum

end;

Funcs F₁(),F₂() is finite by FRAENKEL:16;
hence { f where f is Function of F₁(),F₂() : P₁[f] } is finite by A5; :: thesis: verum

end;

end;

end;

hence { f where f is Function of F₁(),F₂() : P₁[f] } is finite ; :: thesis: verum