let f be PartFunc of REAL,REAL; ( dom f is compact & f | (dom f) is continuous implies rng f is compact )
assume that
A1:
dom f is compact
and
A2:
f | (dom f) is continuous
; rng f is compact
now for s1 being Real_Sequence st rng s1 c= rng f holds
ex q2 being Element of bool [:NAT,REAL:] st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )let s1 be
Real_Sequence;
( rng s1 c= rng f implies ex q2 being Element of bool [:NAT,REAL:] st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) )assume A3:
rng s1 c= rng f
;
ex q2 being Element of bool [:NAT,REAL:] st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )defpred S1[
set ,
set ]
means ( $2
in dom f &
f . $2
= s1 . $1 );
A4:
for
n being
Element of
NAT ex
p being
Element of
REAL st
S1[
n,
p]
consider q1 being
Real_Sequence such that A6:
for
n being
Element of
NAT holds
S1[
n,
q1 . n]
from FUNCT_2:sch 3(A4);
then A7:
rng q1 c= dom f
;
then consider s2 being
Real_Sequence such that A8:
s2 is
subsequence of
q1
and A9:
s2 is
convergent
and A10:
lim s2 in dom f
by A1, RCOMP_1:def 3;
then A11:
f /* q1 = s1
by FUNCT_2:63;
take q2 =
f /* s2;
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
lim s2 in dom (f | (dom f))
by A10;
then
f | (dom f) is_continuous_in lim s2
by A2;
then A12:
f is_continuous_in lim s2
;
rng s2 c= rng q1
by A8, VALUED_0:21;
then A13:
rng s2 c= dom f
by A7;
then
f . (lim s2) = lim (f /* s2)
by A9, A12;
hence
(
q2 is
subsequence of
s1 &
q2 is
convergent &
lim q2 in rng f )
by A7, A11, A8, A9, A10, A12, A13, FUNCT_1:def 3, VALUED_0:22;
verum end;
hence
rng f is compact
by RCOMP_1:def 3; verum