let f be PartFunc of REAL, the carrier of S; :: thesis: ( f is constant implies f is Lipschitzian )
assume A1: f is constant ; :: thesis: f is Lipschitzian

now

let x1, x2 be real number ; :: thesis: ( x1 in dom f & x2 in dom f implies ||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2)) )
assume X1: ( x1 in dom f & x2 in dom f ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2))
then f /. x1 = f . x1 by PARTFUN1:def 8
.= f . x2 by A1, X1, FUNCT_1:def 16
.= f /. x2 by X1, PARTFUN1:def 8 ;
then ||.((f /. x1) - (f /. x2)).|| = 0 by NORMSP_1:10;
hence ||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2)) by COMPLEX1:132; :: thesis: verum

end;

hence f is Lipschitzian by Def3; :: thesis: verum