theorem :: NFCONT_3:30

for X being set
for p being Real
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian