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 A1: ( 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,(REAL-NS n) by REAL_NS1:def 4;
g | Y is continuous by A1, Th23;
hence Z is compact by A1, NFCONT_3:25; :: thesis: verum