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