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