set F = { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } ;

per cases
( F_{2}() < F_{1}() or F_{1}() <= F_{2}() )
;

end;

suppose A1:
F_{2}() < F_{1}()
; :: thesis: { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } is finite

_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } as empty set ;

F is finite ;

hence { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } is finite
; :: thesis: verum

end;

now :: thesis: not { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } <> {}

then reconsider F = { Fassume
{ F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } <> {}
; :: thesis: contradiction

then consider x being object such that

A2: x in { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) }
by XBOOLE_0:def 1;

ex i being Element of INT st

( x = F_{3}(i) & F_{1}() <= i & i <= F_{2}() & P_{1}[i] )
by A2;

hence contradiction by A1, XXREAL_0:2; :: thesis: verum

end;then consider x being object such that

A2: x in { F

ex i being Element of INT st

( x = F

hence contradiction by A1, XXREAL_0:2; :: thesis: verum

F is finite ;

hence { F

suppose
F_{1}() <= F_{2}()
; :: thesis: { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } is finite

then reconsider k = F_{2}() - F_{1}() as Element of NAT by INT_1:5;

set F = { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } ;

defpred S_{1}[ object , object ] means ex i being Integer st

( $1 = i & $2 = F_{3}((i + F_{1}())) );

A3: for e being object st e in k + 1 holds

ex u being object st S_{1}[e,u]

A4: dom f = k + 1 and

A5: for i being object st i in k + 1 holds

S_{1}[i,f . i]
from CLASSES1:sch 1(A3);

A6: { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } c= rng f

hence { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } is finite
by A6; :: thesis: verum

end;set F = { F

defpred S

( $1 = i & $2 = F

A3: for e being object st e in k + 1 holds

ex u being object st S

proof

consider f being Function such that
let e be object ; :: thesis: ( e in k + 1 implies ex u being object st S_{1}[e,u] )

assume e in k + 1 ; :: thesis: ex u being object st S_{1}[e,u]

then e in Segm (k + 1) ;

then reconsider i = e as Nat ;

take F_{3}((i + F_{1}()))
; :: thesis: S_{1}[e,F_{3}((i + F_{1}()))]

take i ; :: thesis: ( e = i & F_{3}((i + F_{1}())) = F_{3}((i + F_{1}())) )

thus ( e = i & F_{3}((i + F_{1}())) = F_{3}((i + F_{1}())) )
; :: thesis: verum

end;assume e in k + 1 ; :: thesis: ex u being object st S

then e in Segm (k + 1) ;

then reconsider i = e as Nat ;

take F

take i ; :: thesis: ( e = i & F

thus ( e = i & F

A4: dom f = k + 1 and

A5: for i being object st i in k + 1 holds

S

A6: { F

proof

rng f is finite
by A4, FINSET_1:8;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) } or x in rng f )

assume x in { F_{3}(i) where i is Element of INT : ( F_{1}() <= i & i <= F_{2}() & P_{1}[i] ) }
; :: thesis: x in rng f

then consider j being Element of INT such that

A7: x = F_{3}(j)
and

A8: F_{1}() <= j
and

A9: j <= F_{2}()
and

P_{1}[j]
;

reconsider l = j - F_{1}() 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_{1}[j - F_{1}(),f . (j - F_{1}())]
by A5;

then f . (j - F_{1}()) =
F_{3}(((j + F_{1}()) - F_{1}()))

.= F_{3}(j)
;

hence x in rng f by A4, A7, A10, FUNCT_1:def 3; :: thesis: verum

end;assume x in { F

then consider j being Element of INT such that

A7: x = F

A8: F

A9: j <= F

P

reconsider l = j - F

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

then f . (j - F

.= F

hence x in rng f by A4, A7, A10, FUNCT_1:def 3; :: thesis: verum

hence { F