theorem :: NFCONT_4:32

for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for Y being Subset of REAL
for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds
Z is compact