let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S

for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds

f .: Y is compact

let f be PartFunc of REAL, the carrier of S; :: thesis: for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds

f .: Y is compact

let Y be Subset of REAL; :: thesis: ( Y c= dom f & Y is compact & f | Y is continuous implies f .: Y is compact )

assume that

A1: Y c= dom f and

A2: Y is compact and

A3: f | Y is continuous ; :: thesis: f .: Y is compact

A4: (f | Y) | Y is continuous by A3;

dom (f | Y) = (dom f) /\ Y by RELAT_1:61

.= Y by A1, XBOOLE_1:28 ;

then rng (f | Y) is compact by A2, A4, Th24;

hence f .: Y is compact by RELAT_1:115; :: thesis: verum

for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds

f .: Y is compact

let f be PartFunc of REAL, the carrier of S; :: thesis: for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds

f .: Y is compact

let Y be Subset of REAL; :: thesis: ( Y c= dom f & Y is compact & f | Y is continuous implies f .: Y is compact )

assume that

A1: Y c= dom f and

A2: Y is compact and

A3: f | Y is continuous ; :: thesis: f .: Y is compact

A4: (f | Y) | Y is continuous by A3;

dom (f | Y) = (dom f) /\ Y by RELAT_1:61

.= Y by A1, XBOOLE_1:28 ;

then rng (f | Y) is compact by A2, A4, Th24;

hence f .: Y is compact by RELAT_1:115; :: thesis: verum