let CNS be ComplexNormSpace; :: thesis: for Y being Subset of CNS holds id Y is_Lipschitzian_on Y
let Y be Subset of CNS; :: thesis: id Y is_Lipschitzian_on Y
thus Y c= dom (id Y) by RELAT_1:71; :: according to NCFCONT1:def 27 :: thesis: ex r being Real st
( 0 < r & ( for x1, x2 being Point of CNS st x1 in Y & x2 in Y holds
||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ) )
reconsider r = 1 as Real ;
take r ; :: thesis: ( 0 < r & ( for x1, x2 being Point of CNS st x1 in Y & x2 in Y holds
||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ) )
thus r > 0 ; :: thesis: for x1, x2 being Point of CNS st x1 in Y & x2 in Y holds
||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).||
let x1, x2 be Point of CNS; :: thesis: ( x1 in Y & x2 in Y implies ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| )
assume A1: ( x1 in Y & x2 in Y ) ; :: thesis: ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).||
then ||.(((id Y) /. x1) - ((id Y) /. x2)).|| = ||.(x1 - ((id Y) /. x2)).|| by PARTFUN2:12
.= r * ||.(x1 - x2).|| by A1, PARTFUN2:12 ;
hence ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ; :: thesis: verum