set F = { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } ;
now :: thesis: { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } is finite
per cases ( F2() = 0 or F2() > 0 ) ;
suppose A1: F2() = 0 ; :: thesis: { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } is finite
{ f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } c=
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } or x in )
assume x in { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } ; :: thesis:
then consider f being Function of F1(),F2() such that
A2: x = f and
P1[f] ;
f = {} by A1;
hence x in by ; :: thesis: verum
end;
hence { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } is finite ; :: thesis: verum
end;
suppose A3: F2() > 0 ; :: thesis: { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } is finite
A4: { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } c= Funcs (F1(),F2())
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } or x in Funcs (F1(),F2()) )
assume x in { f where f is Function of (Segm F1()),(Segm 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 ; :: thesis: verum
end;
Funcs (F1(),F2()) is finite by FRAENKEL:6;
hence { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } is finite by A4; :: thesis: verum
end;
end;
end;
hence { f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } is finite ; :: thesis: verum