reconsider g1 = f1, g2 = f2 as PartFunc of REAL, the carrier of (REAL-NS n) by REAL_NS1:def 4;
P1: ( g1 is Lipschitzian & g2 is Lipschitzian ) by Def6Th1;
g1 - g2 = f1 - f2 by LM003D;
hence for b₁ being PartFunc of REAL,(REAL n) st b₁ = f1 - f2 holds
b₁ is Lipschitzian by P1, Def6Th1; :: thesis: verum