let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for Y being Subset of CNS
for f being PartFunc of CNS,RNS st Y c= dom f & Y is compact & f is_continuous_on Y holds
f .: Y is compact
let RNS be RealNormSpace; :: thesis: for Y being Subset of CNS
for f being PartFunc of CNS,RNS st Y c= dom f & Y is compact & f is_continuous_on Y holds
f .: Y is compact
let Y be Subset of CNS; :: thesis: for f being PartFunc of CNS,RNS st Y c= dom f & Y is compact & f is_continuous_on Y holds
f .: Y is compact
let f be PartFunc of CNS,RNS; :: thesis: ( Y c= dom f & Y is compact & f is_continuous_on Y implies f .: Y is compact )
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f is_continuous_on Y ; :: thesis: f .: Y is compact
A4: dom (f | Y) = (dom f) /\ Y by RELAT_1:61
.= Y by A1, XBOOLE_1:28 ;
f | Y is_continuous_on Y

proof

thus Y c= dom (f | Y) by A4; :: according to NCFCONT1:def 12 :: thesis: for x0 being Point of CNS st x0 in Y holds
(f | Y) | Y is_continuous_in x0
let r be Point of CNS; :: thesis: ( r in Y implies (f | Y) | Y is_continuous_in r )
assume r in Y ; :: thesis: (f | Y) | Y is_continuous_in r
then f | Y is_continuous_in r by A3;
hence (f | Y) | Y is_continuous_in r by RELAT_1:72; :: thesis: verum

end;

then rng (f | Y) is compact by A2, A4, Th78;
hence f .: Y is compact by RELAT_1:115; :: thesis: verum