consider x being Point of M;
reconsider f = the carrier of M --> x as Function of the carrier of M,the carrier of M ;
take f ; :: thesis: ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) )
take 1 / 2 ; :: thesis: ( 0 < 1 / 2 & 1 / 2 < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= (1 / 2) * ||.(x - y).|| ) )
thus ( 0 < 1 / 2 & 1 / 2 < 1 ) ; :: thesis: for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= (1 / 2) * ||.(x - y).||
let z, y be Point of M; :: thesis: ||.((f . z) - (f . y)).|| <= (1 / 2) * ||.(z - y).||
( f . z = x & f . y = x ) by FUNCOP_1:13;
then A1: ||.((f . z) - (f . y)).|| = 0 by CLVECT_1:108;
||.(z - y).|| >= 0 by CLVECT_1:106;
hence ||.((f . z) - (f . y)).|| <= (1 / 2) * ||.(z - y).|| by A1; :: thesis: verum