set F = { f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] } ;

_{1}()),(Segm F_{2}()) : P_{1}[f] } is finite
; :: thesis: verum

now :: thesis: { f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] } is finite end;

hence
{ f where f is Function of (Segm Fper cases
( F_{2}() = 0 or F_{2}() > 0 )
;

end;

suppose A1:
F_{2}() = 0
; :: thesis: { f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] } is finite

{ f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] } c= {{}}
_{1}()),(Segm F_{2}()) : P_{1}[f] } is finite
; :: thesis: verum

end;proof

hence
{ f where f is Function of (Segm F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] } or x in {{}} )

assume x in { f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] }
; :: thesis: x in {{}}

then consider f being Function of F_{1}(),F_{2}() such that

A2: x = f and

P_{1}[f]
;

f = {} by A1;

hence x in {{}} by A2, TARSKI:def 1; :: thesis: verum

end;assume x in { f where f is Function of (Segm F

then consider f being Function of F

A2: x = f and

P

f = {} by A1;

hence x in {{}} by A2, TARSKI:def 1; :: thesis: verum

suppose A3:
F_{2}() > 0
; :: thesis: { f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] } is finite

A4:
{ f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] } c= Funcs (F_{1}(),F_{2}())
_{1}(),F_{2}()) is finite
by FRAENKEL:6;

hence { f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] } is finite
by A4; :: thesis: verum

end;proof

Funcs (F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] } or x in Funcs (F_{1}(),F_{2}()) )

assume x in { f where f is Function of (Segm F_{1}()),(Segm F_{2}()) : P_{1}[f] }
; :: thesis: x in Funcs (F_{1}(),F_{2}())

then ex f being Function of F_{1}(),F_{2}() st

( x = f & P_{1}[f] )
;

hence x in Funcs (F_{1}(),F_{2}())
by A3, FUNCT_2:8; :: thesis: verum

end;assume x in { f where f is Function of (Segm F

then ex f being Function of F

( x = f & P

hence x in Funcs (F

hence { f where f is Function of (Segm F