theorem Th112: :: NCFCONT1:112

for CNS1, CNS2 being ComplexNormSpace
for X being set
for f being PartFunc of CNS1,CNS2 st X c= dom f & f | X is constant holds
f is_Lipschitzian_on X