reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
A1: g is Lipschitzian by Th34;
p (#) g = p (#) f by Th6;
hence for b₁ being PartFunc of REAL,(REAL n) st b₁ = p (#) f holds
b₁ is Lipschitzian by A1; :: thesis: verum