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

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