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 AS: ( f | X is Lipschitzian & X c= dom f ) ; :: thesis: (p (#) f) | X is Lipschitzian
reconsider g = f as PartFunc of REAL, the carrier of (REAL-NS n) by REAL_NS1:def 4;
g | X is Lipschitzian by Def6Th1, AS;
then P1: (p (#) g) | X is Lipschitzian by AS, NFCONT_3:30;
p (#) g = p (#) f by LM003B;
hence (p (#) f) | X is Lipschitzian by P1, Def6Th1; :: thesis: verum