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

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

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

now

assume { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } <> {} ; :: thesis: contradiction
then consider x being set such that
W: 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 W;
hence contradiction by S, 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 S: F₁() <= F₂() ; :: thesis: { F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } is finite

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

proof

let e be set ; :: thesis: ( e in k + 1 implies ex u being set st S₁[e,u] )
assume e in k + 1 ; :: thesis: ex u being set st S₁[e,u]
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
A1: dom f = k + 1 and
A2: for i being set st i in k + 1 holds
S₁[i,f . i] from CLASSES1:sch 1(X);
X: rng f is finite by A1, FINSET_1:26;
{ F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } c= rng f

proof

let x be set ; :: 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
W1: x = F₃(j) and
W2: ( F₁() <= j & j <= F₂() ) and
P₁[j] ;
reconsider l = j - F₁() as Element of NAT by W2, INT_1:18;
l <= k by W2, XREAL_1:11;
then l < k + 1 by NAT_1:13;
then B: l in k + 1 by NAT_1:45;
S₁[j - F₁(),f . (j - F₁())] by B, A2;
then f . (j - F₁()) = F₃(((j + F₁()) - F₁()))
.= F₃(j) ;
hence x in rng f by W1, A1, B, FUNCT_1:def 5; :: thesis: verum

end;

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

end;

end;