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