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

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