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