let X be set ; :: thesis: for p being real number
for f being PartFunc of REAL ,REAL st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
let p be real number ; :: thesis: for f being PartFunc of REAL ,REAL st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
let f be PartFunc of REAL ,REAL ; :: thesis: ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian )
(p (#) f) | X = p (#) (f | X) by RFUNCT_1:65;
hence ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian ) ; :: thesis: verum