for S, T, V being RealNormSpace
for x0 being Point of V
for f1 being PartFunc of the carrier of V, 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