let S be RealNormSpace; :: thesis: for Y being Subset of S holds id Y is_Lipschitzian_on Y
let Y be Subset of S; :: thesis: id Y is_Lipschitzian_on Y
reconsider r = 1 as Real ;
thus Y c= dom (id Y) by RELAT_1:45; :: according to NFCONT_1:def 9 :: thesis: ex r being Real st
( 0 < r & ( for x1, x2 being Point of S st x1 in Y & x2 in Y holds
||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ) )
take r ; :: thesis: ( 0 < r & ( for x1, x2 being Point of S 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 S st x1 in Y & x2 in Y holds
||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).||
let x1, x2 be Point of S; :: thesis: ( x1 in Y & x2 in Y implies ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| )
assume that
A1: x1 in Y and
A2: x2 in Y ; :: thesis: ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).||
||.(((id Y) /. x1) - ((id Y) /. x2)).|| = ||.(x1 - ((id Y) /. x2)).|| by A1, PARTFUN2:6
.= r * ||.(x1 - x2).|| by A2, PARTFUN2:6 ;
hence ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ; :: thesis: verum