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

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