reconsider r = 1 as Real ;

id Y is Lipschitzian_{1} being PartFunc of REAL,REAL st b_{1} = id Y holds

b_{1} is Lipschitzian
; :: thesis: verum

id Y is Lipschitzian

proof

hence
for b
take
r
; :: according to FCONT_1:def 3 :: thesis: ( 0 < r & ( for x1, x2 being Real st x1 in dom (id Y) & x2 in dom (id Y) holds

|.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).| ) )

thus r > 0 ; :: thesis: for x1, x2 being Real st x1 in dom (id Y) & x2 in dom (id Y) holds

|.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).|

let x1, x2 be Real; :: thesis: ( x1 in dom (id Y) & x2 in dom (id Y) implies |.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).| )

assume that

A1: x1 in dom (id Y) and

A2: x2 in dom (id Y) ; :: thesis: |.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).|

A3: x2 in Y by A2;

x1 in Y by A1;

then |.(((id Y) . x1) - ((id Y) . x2)).| = |.(x1 - ((id Y) . x2)).| by FUNCT_1:18

.= r * |.(x1 - x2).| by A3, FUNCT_1:18 ;

hence |.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).| ; :: thesis: verum

end;|.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).| ) )

thus r > 0 ; :: thesis: for x1, x2 being Real st x1 in dom (id Y) & x2 in dom (id Y) holds

|.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).|

let x1, x2 be Real; :: thesis: ( x1 in dom (id Y) & x2 in dom (id Y) implies |.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).| )

assume that

A1: x1 in dom (id Y) and

A2: x2 in dom (id Y) ; :: thesis: |.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).|

A3: x2 in Y by A2;

x1 in Y by A1;

then |.(((id Y) . x1) - ((id Y) . x2)).| = |.(x1 - ((id Y) . x2)).| by FUNCT_1:18

.= r * |.(x1 - x2).| by A3, FUNCT_1:18 ;

hence |.(((id Y) . x1) - ((id Y) . x2)).| <= r * |.(x1 - x2).| ; :: thesis: verum

b