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,(REAL-NS n) by REAL_NS1:def 4;
g is constant by A1;
hence f is Lipschitzian ; :: thesis: verum