let X, X1 be set ; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | X1 is continuous holds
(f2 * f1) | (X /\ (f1 " X1)) is continuous
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 | X is continuous & f2 | X1 is continuous implies (f2 * f1) | (X /\ (f1 " X1)) is continuous )
(f2 | X1) * (f1 | X) = (f2 * f1) | (X /\ (f1 " X1)) by FUNCT_1:100;
hence ( f1 | X is continuous & f2 | X1 is continuous implies (f2 * f1) | (X /\ (f1 " X1)) is continuous ) ; :: thesis: verum