let n be Element of NAT ; :: thesis: 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
let f be PartFunc of REAL,(REAL n); :: thesis: 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
let Y be Subset of REAL; :: thesis: 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
let Z be Subset of (REAL-NS n); :: thesis: ( Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous implies Z is compact )
assume AS: ( Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous ) ; :: thesis: Z is compact
reconsider g = f as PartFunc of REAL, the carrier of (REAL-NS n) by REAL_NS1:def 4;
g | Y is continuous by AS, Def2Th;
hence Z is compact by AS, NFCONT_3:25; :: thesis: verum