let f be PartFunc of REAL,REAL; :: thesis: ( 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 ; :: thesis: rng f is compact

assume that

A1: dom f is compact and

A2: f | (dom f) is continuous ; :: thesis: rng f is compact

now :: thesis: 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 )

hence
rng f is compact
by RCOMP_1:def 3; :: thesis: verumex 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; :: thesis: ( 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 ; :: thesis: ex q2 being Element of bool [:NAT,REAL:] st

( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )

defpred S_{1}[ 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 S_{1}[n,p]

A6: for n being Element of NAT holds S_{1}[n,q1 . n]
from FUNCT_2:sch 3(A4);

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;

take q2 = f /* s2; :: thesis: ( 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; :: thesis: verum

end;( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) )

assume A3: rng s1 c= rng f ; :: thesis: ex q2 being Element of bool [:NAT,REAL:] st

( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )

defpred S

A4: for n being Element of NAT ex p being Element of REAL st S

proof

consider q1 being Real_Sequence such that
let n be Element of NAT ; :: thesis: ex p being Element of REAL st S_{1}[n,p]

s1 . n in rng s1 by VALUED_0:28;

then consider p being Element of REAL such that

A5: ( p in dom f & s1 . n = f . p ) by A3, PARTFUN1:3;

take p ; :: thesis: S_{1}[n,p]

thus S_{1}[n,p]
by A5; :: thesis: verum

end;s1 . n in rng s1 by VALUED_0:28;

then consider p being Element of REAL such that

A5: ( p in dom f & s1 . n = f . p ) by A3, PARTFUN1:3;

take p ; :: thesis: S

thus S

A6: for n being Element of NAT holds S

now :: thesis: for x being object st x in rng q1 holds

x in dom f

then A7:
rng q1 c= dom f
;x in dom f

let x be object ; :: thesis: ( x in rng q1 implies x in dom f )

assume x in rng q1 ; :: thesis: x in dom f

then ex n being Element of NAT st x = q1 . n by FUNCT_2:113;

hence x in dom f by A6; :: thesis: verum

end;assume x in rng q1 ; :: thesis: x in dom f

then ex n being Element of NAT st x = q1 . n by FUNCT_2:113;

hence x in dom f by A6; :: thesis: verum

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;

now :: thesis: for n being Element of NAT holds (f /* q1) . n = s1 . n

then A11:
f /* q1 = s1
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (f /* q1) . n = s1 . n

f . (q1 . n) = s1 . n by A6;

hence (f /* q1) . n = s1 . n by A7, FUNCT_2:108; :: thesis: verum

end;f . (q1 . n) = s1 . n by A6;

hence (f /* q1) . n = s1 . n by A7, FUNCT_2:108; :: thesis: verum

take q2 = f /* s2; :: thesis: ( 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; :: thesis: verum