let n be Element of NAT ; :: thesis: for X being set

for p being Real

for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds

(p (#) f) | X is Lipschitzian

let X be set ; :: thesis: for p being Real

for f being PartFunc of REAL,(REAL n) 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 n) st f | X is Lipschitzian & X c= dom f holds

(p (#) f) | X is Lipschitzian

let f be PartFunc of REAL,(REAL n); :: thesis: ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian )

assume A1: ( f | X is Lipschitzian & X c= dom f ) ; :: thesis: (p (#) f) | X is Lipschitzian

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

A2: (p (#) g) | X is Lipschitzian by A1, NFCONT_3:30;

p (#) g = p (#) f by Th6;

hence (p (#) f) | X is Lipschitzian by A2; :: thesis: verum

for p being Real

for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds

(p (#) f) | X is Lipschitzian

let X be set ; :: thesis: for p being Real

for f being PartFunc of REAL,(REAL n) 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 n) st f | X is Lipschitzian & X c= dom f holds

(p (#) f) | X is Lipschitzian

let f be PartFunc of REAL,(REAL n); :: thesis: ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian )

assume A1: ( f | X is Lipschitzian & X c= dom f ) ; :: thesis: (p (#) f) | X is Lipschitzian

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

A2: (p (#) g) | X is Lipschitzian by A1, NFCONT_3:30;

p (#) g = p (#) f by Th6;

hence (p (#) f) | X is Lipschitzian by A2; :: thesis: verum