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

now :: thesis: { f where f is Function of (Segm F₁()),(Segm F₂()) : P₁[f] } is finite

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

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

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

proof

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

end;

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

end;

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

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

proof

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

end;

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

end;

end;

end;

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