let X be set ; :: thesis: for p being Real
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; :: 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:49;
hence ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian ) ; :: thesis: verum