now

let x0 be real number ; :: thesis: ( x0 in dom (f2 * f1) implies f2 * f1 is_continuous_in x0 )
assume Z1: x0 in dom (f2 * f1) ; :: thesis: f2 * f1 is_continuous_in x0
then x0 in dom f1 by FUNCT_1:21;
then Z2: f1 is_continuous_in x0 by Def2;
f1 . x0 in dom f2 by Z1, FUNCT_1:21;
then f2 is_continuous_in f1 . x0 by Def2;
hence f2 * f1 is_continuous_in x0 by Z1, Z2, Th12; :: thesis: verum

end;

hence f2 * f1 is continuous PartFunc of REAL , REAL by Def2; :: thesis: verum