reconsider r = 1 as Real ;
id Y is Lipschitzian

proof

take r ; :: according to FCONT_1:def 3 :: thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (id Y) & x2 in dom (id Y) holds
abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2)) ) )
thus r > 0 ; :: thesis: for x1, x2 being real number st x1 in dom (id Y) & x2 in dom (id Y) holds
abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2))
let x1, x2 be real number ; :: thesis: ( x1 in dom (id Y) & x2 in dom (id Y) implies abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2)) )
assume that
A1: x1 in dom (id Y) and
A2: x2 in dom (id Y) ; :: thesis: abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2))
A3: x2 in Y by A2, RELAT_1:45;
x1 in Y by A1, RELAT_1:45;
then abs (((id Y) . x1) - ((id Y) . x2)) = abs (x1 - ((id Y) . x2)) by FUNCT_1:18
.= r * (abs (x1 - x2)) by A3, FUNCT_1:18 ;
hence abs (((id Y) . x1) - ((id Y) . x2)) <= r * (abs (x1 - x2)) ; :: thesis: verum

end;

hence for b₁ being PartFunc of REAL,REAL st b₁ = id Y holds
b₁ is Lipschitzian ; :: thesis: verum