set F = { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } ;

per cases ( F₂() < F₁() or F₁() <= F₂() ) ;

suppose A1: F₂() < F₁() ; :: thesis: { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } is finite

now :: thesis: not { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } <> {}

assume { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } by XBOOLE_0:def 1;
ex i being Element of INT st
( x = F₃(i) & F₁() <= i & i <= F₂() & P₁[i] ) by A2;
hence contradiction by A1, XXREAL_0:2; :: thesis: verum

end;

then reconsider F = { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } as empty set ;
F is finite ;
hence { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } is finite ; :: thesis: verum

end;

suppose F₁() <= F₂() ; :: thesis: { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } is finite

then reconsider k = F₂() - F₁() as Element of NAT by INT_1:5;
set F = { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } ;
defpred S₁[ object , object ] means ex i being Integer st
( $1 = i & $2 = F₃((i + F₁())) );
A3: for e being object st e in k + 1 holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in k + 1 implies ex u being object st S₁[e,u] )
assume e in k + 1 ; :: thesis: ex u being object st S₁[e,u]
then e in Segm (k + 1) ;
then reconsider i = e as Nat ;
take F₃((i + F₁())) ; :: thesis: S₁[e,F₃((i + F₁()))]
take i ; :: thesis: ( e = i & F₃((i + F₁())) = F₃((i + F₁())) )
thus ( e = i & F₃((i + F₁())) = F₃((i + F₁())) ) ; :: thesis: verum

end;

consider f being Function such that
A4: dom f = k + 1 and
A5: for i being object st i in k + 1 holds
S₁[i,f . i] from CLASSES1:sch 1(A3);
A6: { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } or x in rng f )
assume x in { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } ; :: thesis: x in rng f
then consider j being Element of INT such that
A7: x = F₃(j) and
A8: F₁() <= j and
A9: j <= F₂() and
P₁[j] ;
reconsider l = j - F₁() as Element of NAT by A8, INT_1:5;
l <= k by A9, XREAL_1:9;
then l < k + 1 by NAT_1:13;
then A10: l in Segm (k + 1) by NAT_1:44;
then S₁[j - F₁(),f . (j - F₁())] by A5;
then f . (j - F₁()) = F₃(((j + F₁()) - F₁()))
.= F₃(j) ;
hence x in rng f by A4, A7, A10, FUNCT_1:def 3; :: thesis: verum

end;

rng f is finite by A4, FINSET_1:8;
hence { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } is finite by A6; :: thesis: verum

end;

end;