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
Z1: f | X is continuous and
Z2: (f | X) " {0 } = {} ; :: thesis: (f ^ ) | X is continuous
(f | X) | X is continuous by Z1;
then ((f | X) ^ ) | X is continuous by Th23, Z2;
then ((f ^ ) | X) | X is continuous by RFUNCT_1:62;
hence (f ^ ) | X is continuous by RELAT_1:101; :: thesis: verum