let S be RealNormSpace; :: thesis: for f being PartFunc of the carrier of S,REAL st dom f is compact & f is_continuous_on dom f holds
rng f is compact
let f be PartFunc of the carrier of S,REAL; :: thesis: ( dom f is compact & f is_continuous_on dom f implies rng f is compact )
assume that
A1: dom f is compact and
A2: f is_continuous_on dom f ; :: thesis: rng f is compact
now :: thesis: for s1 being Real_Sequence st rng s1 c= rng f holds
ex q2 being Element of K16(K17(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 K16(K17(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 K16(K17(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 Point of S st S1[n,p]
proof
let n be Element of NAT ; :: thesis: ex p being Point of S st S1[n,p]
dom s1 = NAT by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:3;
then consider p being Point of S such that
A5: ( p in dom f & s1 . n = f . p ) by A3, PARTFUN1:3;
take p ; :: thesis: S1[n,p]
thus S1[n,p] by A5, PARTFUN1:def 6; :: thesis: verum
end;
consider q1 being sequence of S such that
A6: for n being Element of NAT holds S1[n,q1 . n] from FUNCT_2:sch 3(A4);
now :: thesis: for x being object st x in rng q1 holds
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 consider n being Nat such that
A7: x = q1 . n by Th6;
n in NAT by ORDINAL1:def 12;
hence x in dom f by A6, A7; :: thesis: verum
end;
then A8: rng q1 c= dom f ;
then consider s2 being sequence of S such that
A9: s2 is subsequence of q1 and
A10: s2 is convergent and
A11: lim s2 in dom f by A1;
take q2 = f /* s2; :: thesis: ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
rng s2 c= rng q1 by A9, VALUED_0:21;
then A12: rng s2 c= dom f by A8;
now :: thesis: for n being Element of NAT holds (f /* q1) . n = s1 . n
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 A8, FUNCT_2:109; :: thesis: verum
end;
then A13: f /* q1 = s1 by FUNCT_2:63;
f | (dom f) is_continuous_in lim s2 by A2, A11;
then A14: f is_continuous_in lim s2 by RELAT_1:68;
then f /. (lim s2) = lim (f /* s2) by A10, A12;
hence ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) by A8, A13, A9, A10, A14, A12, PARTFUN2:2, VALUED_0:22; :: thesis: verum
end;
hence rng f is compact by RCOMP_1:def 3; :: thesis: verum