for CNS being ComplexNormSpace
for Y being Subset of CNS holds id Y is_Lipschitzian_on Y