let X be set ; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | (f1 .: X) is continuous holds

(f2 * f1) | X is continuous

let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 | X is continuous & f2 | (f1 .: X) is continuous implies (f2 * f1) | X is continuous )

(f2 * f1) | X = (f2 | (f1 .: X)) * (f1 | X) by FUNCT_1:99;

hence ( f1 | X is continuous & f2 | (f1 .: X) is continuous implies (f2 * f1) | X is continuous ) ; :: thesis: verum

(f2 * f1) | X is continuous

let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 | X is continuous & f2 | (f1 .: X) is continuous implies (f2 * f1) | X is continuous )

(f2 * f1) | X = (f2 | (f1 .: X)) * (f1 | X) by FUNCT_1:99;

hence ( f1 | X is continuous & f2 | (f1 .: X) is continuous implies (f2 * f1) | X is continuous ) ; :: thesis: verum