let n be Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)
for Y being Subset of (REAL-NS n) st dom f is compact & f | (dom f) is continuous & Y = rng f holds
Y is compact
let f be PartFunc of REAL,(REAL n); :: thesis: for Y being Subset of (REAL-NS n) st dom f is compact & f | (dom f) is continuous & Y = rng f holds
Y is compact
let Y be Subset of (REAL-NS n); :: thesis: ( dom f is compact & f | (dom f) is continuous & Y = rng f implies Y is compact )
assume A1: ( dom f is compact & f | (dom f) is continuous & Y = rng f ) ; :: thesis: Y is compact
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
g | (dom g) is continuous by A1, Th23;
hence Y is compact by A1, NFCONT_3:24; :: thesis: verum