now :: thesis: for x0 being Real st x0 in dom (f2 * f1) holds
f2 * f1 is_continuous_in x0

let x0 be Real; :: thesis: ( x0 in dom (f2 * f1) implies f2 * f1 is_continuous_in x0 )
assume A1: x0 in dom (f2 * f1) ; :: thesis: f2 * f1 is_continuous_in x0
then f1 . x0 in dom f2 by FUNCT_1:11;
then A2: f2 is_continuous_in f1 . x0 by Def2;
x0 in dom f1 by A1, FUNCT_1:11;
then f1 is_continuous_in x0 by Def2;
hence f2 * f1 is_continuous_in x0 by A1, A2, Th12; :: thesis: verum

end;

hence for b₁ being PartFunc of REAL,REAL st b₁ = f2 * f1 holds
b₁ is continuous ; :: thesis: verum