for S, T being RealNormSpace
for f1 being PartFunc of S,REAL
for f2 being PartFunc of REAL,T
for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0