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

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