set F = { f where f is Function of F1(),F2() : P1[f] } ;
now
per cases ( F2() = 0 or F2() > 0 ) ;
suppose A1: F2() = 0 ; :: thesis: { f where f is Function of F1(),F2() : P1[f] } is finite
{ f where f is Function of F1(),F2() : P1[f] } c= {{} }
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F1(),F2() : P1[f] } or x in {{} } )
assume x in { f where f is Function of F1(),F2() : P1[f] } ; :: thesis: x in {{} }
then consider f being Function of F1(),F2() such that
A2: x = f and
P1[f] ;
 f = {} by A1;
hence x in {{} } by A2, TARSKI:def 1; :: thesis: verum
end;
hence { f where f is Function of F1(),F2() : P1[f] } is finite ; :: thesis: verum
end;
suppose A3: F2() > 0 ; :: thesis: { f where f is Function of F1(),F2() : P1[f] } is finite
A4: { f where f is Function of F1(),F2() : P1[f] } c= Funcs F1(),F2()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F1(),F2() : P1[f] } or x in Funcs F1(),F2() )
assume x in { f where f is Function of F1(),F2() : P1[f] } ; :: thesis: x in Funcs F1(),F2()
then ex f being Function of F1(),F2() st
( x = f & P1[f] ) ;
hence x in Funcs F1(),F2() by A3, FUNCT_2:11; :: thesis: verum
end;
Funcs F1(),F2() is finite by FRAENKEL:16;
hence { f where f is Function of F1(),F2() : P1[f] } is finite by A4; :: thesis: verum
end;
end;
end;
hence { f where f is Function of F1(),F2() : P1[f] } is finite ; :: thesis: verum