set F = { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } ;
per cases ( F2() < F1() or F1() <= F2() ) ;
suppose A1: F2() < F1() ; :: thesis: { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } is finite
now :: thesis: not { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } <> {}
assume { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } by XBOOLE_0:def 1;
ex i being Element of INT st
( x = F3(i) & F1() <= i & i <= F2() & P1[i] ) by A2;
hence contradiction by A1, XXREAL_0:2; :: thesis: verum
end;
then reconsider F = { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } as empty set ;
F is finite ;
hence { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } is finite ; :: thesis: verum
end;
suppose F1() <= F2() ; :: thesis: { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } is finite
then reconsider k = F2() - F1() as Element of NAT by INT_1:5;
set F = { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } ;
defpred S1[ object , object ] means ex i being Integer st
( $1 = i & $2 = F3((i + F1())) );
A3: for e being object st e in k + 1 holds
ex u being object st S1[e,u]
proof
let e be object ; :: thesis: ( e in k + 1 implies ex u being object st S1[e,u] )
assume e in k + 1 ; :: thesis: ex u being object st S1[e,u]
then e in Segm (k + 1) ;
then reconsider i = e as Nat ;
take F3((i + F1())) ; :: thesis: S1[e,F3((i + F1()))]
take i ; :: thesis: ( e = i & F3((i + F1())) = F3((i + F1())) )
thus ( e = i & F3((i + F1())) = F3((i + F1())) ) ; :: 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
S1[i,f . i] from CLASSES1:sch 1(A3);
A6: { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } or x in rng f )
assume x in { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } ; :: thesis: x in rng f
then consider j being Element of INT such that
A7: x = F3(j) and
A8: F1() <= j and
A9: j <= F2() and
P1[j] ;
reconsider l = j - F1() 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 S1[j - F1(),f . (j - F1())] by A5;
then f . (j - F1()) = F3(((j + F1()) - F1()))
.= F3(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 { F3(i) where i is Element of INT : ( F1() <= i & i <= F2() & P1[i] ) } is finite by A6; :: thesis: verum
end;
end;