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