let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f | X is continuous & (f | X) " {0} = {} holds

(f ^) | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( f | X is continuous & (f | X) " {0} = {} implies (f ^) | X is continuous )

assume that

A1: f | X is continuous and

A2: (f | X) " {0} = {} ; :: thesis: (f ^) | X is continuous

(f | X) | X is continuous by A1;

then ((f | X) ^) | X is continuous by A2, Th22;

then ((f ^) | X) | X is continuous by RFUNCT_1:46;

hence (f ^) | X is continuous ; :: thesis: verum

(f ^) | X is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( f | X is continuous & (f | X) " {0} = {} implies (f ^) | X is continuous )

assume that

A1: f | X is continuous and

A2: (f | X) " {0} = {} ; :: thesis: (f ^) | X is continuous

(f | X) | X is continuous by A1;

then ((f | X) ^) | X is continuous by A2, Th22;

then ((f ^) | X) | X is continuous by RFUNCT_1:46;

hence (f ^) | X is continuous ; :: thesis: verum