let X be set ; :: thesis: 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
let p be Real; :: thesis: 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
let S be RealNormSpace; :: thesis: 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
let f be PartFunc of REAL, the carrier of S; :: thesis: ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian )
(p (#) f) | X = p (#) (f | X) by VFUNCT_1:31;
hence ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian ) ; :: thesis: verum