let f be PartFunc of REAL,(REAL n); :: thesis: ( f is empty implies f is Lipschitzian )
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
assume f is empty ; :: thesis: f is Lipschitzian
then g is empty ;
hence f is Lipschitzian ; :: thesis: verum