let f be PartFunc of COMPLEX ,COMPLEX ; :: 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

let s1 be Complex_Sequence; :: thesis: ( rng s1 c= rng f implies ex q2 being Element of K21(K22(NAT ,COMPLEX )) 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 K21(K22(NAT ,COMPLEX )) st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
defpred S₁[ set , set ] means ( $2 in dom f & f /. $2 = s1 . $1 );
A4: for n being Element of NAT ex g being Element of COMPLEX st S₁[n,g]

proof

let n be Element of NAT ; :: thesis: ex g being Element of COMPLEX st S₁[n,g]
s1 . n in rng s1 by VALUED_0:28;
then consider g being Element of COMPLEX such that
A5: ( g in dom f & s1 . n = f . g ) by A3, PARTFUN1:26;
take g ; :: thesis: S₁[n,g]
thus S₁[n,g] by A5, PARTFUN1:def 8; :: thesis: verum

end;

consider q1 being Complex_Sequence such that
A6: for n being Element of NAT holds S₁[n,q1 . n] from CFCONT_1:sch 1(A4);

now

let x be set ; :: 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:190;
hence x in dom f by A6; :: thesis: verum

end;

then A7: rng q1 c= dom f by TARSKI:def 3;

now

let n be Element of NAT ; :: thesis: (f /* q1) . n = s1 . n
( q1 . n in dom f & f /. (q1 . n) = s1 . n ) by A6;
hence (f /* q1) . n = s1 . n by A7, FUNCT_2:186; :: thesis: verum

end;

then A8: f /* q1 = s1 by FUNCT_2:113;
consider s2 being Complex_Sequence such that
A9: ( s2 is subsequence of q1 & s2 is convergent & lim s2 in dom f ) by A1, A7, Def6;
f | (dom f) is_continuous_in lim s2 by A2, A9, Def5;
then A10: f is_continuous_in lim s2 by RELAT_1:97;
rng s2 c= rng q1 by A9, VALUED_0:21;
then rng s2 c= dom f by A7, XBOOLE_1:1;
then ( f /* s2 is convergent & f /. (lim s2) = lim (f /* s2) ) by A9, A10, Def2;
then A11: ( f /* s2 is convergent & f . (lim s2) = lim (f /* s2) ) by A9, PARTFUN1:def 8;
take q2 = f /* s2; :: thesis: ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
thus ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) by A7, A8, A9, A11, FUNCT_1:def 5, VALUED_0:22; :: thesis: verum

end;

hence rng f is compact by Def6; :: thesis: verum