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