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