let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st X c= dom f & f | X is constant holds
f is_Lipschitzian_on X
let RNS be RealNormSpace; :: thesis: for X being set
for f being PartFunc of CNS,RNS st X c= dom f & f | X is constant holds
f is_Lipschitzian_on X
let X be set ; :: thesis: for f being PartFunc of CNS,RNS st X c= dom f & f | X is constant holds
f is_Lipschitzian_on X
let f be PartFunc of CNS,RNS; :: thesis: ( X c= dom f & f | X is constant implies f is_Lipschitzian_on X )
assume that
A1: X c= dom f and
A2: f | X is constant ; :: thesis: f is_Lipschitzian_on X

now :: thesis: for x1, x2 being Point of CNS st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||

let x1, x2 be Point of CNS; :: thesis: ( x1 in X & x2 in X implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| )
assume that
A3: x1 in X and
A4: x2 in X ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||
A5: ( x1 in X /\ (dom f) & x2 in X /\ (dom f) ) by A1, A3, A4, XBOOLE_0:def 4;
f /. x1 = f . x1 by A1, A3, PARTFUN1:def 6
.= f . x2 by A2, A5, PARTFUN2:58
.= f /. x2 by A1, A4, PARTFUN1:def 6 ;
then ||.((f /. x1) - (f /. x2)).|| = ||.(0. RNS).|| by RLVECT_1:15
.= 0 by NORMSP_1:1 ;
hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| by CLVECT_1:105; :: thesis: verum

end;

hence f is_Lipschitzian_on X by A1; :: thesis: verum