set x = the Point of M;
reconsider f = the carrier of M --> the Point of M 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 = the Point of M & f . y = the Point of M ) by FUNCOP_1:7;
then A1: ||.((f . z) - (f . y)).|| = 0 by CLVECT_1:107;
||.(z - y).|| >= 0 by CLVECT_1:105;
hence ||.((f . z) - (f . y)).|| <= (1 / 2) * ||.(z - y).|| by A1; :: thesis: verum