set x = the Point of M;
reconsider f = the carrier of M --> the Point of M as Function of M,M ;
take f ; :: thesis: f is contraction
take 1 / 2 ; :: according to ALI2:def 1 :: thesis: ( 0 < 1 / 2 & 1 / 2 < 1 & ( for x, y being Point of M holds dist ((f . x),(f . y)) <= (1 / 2) * (dist (x,y)) ) )
thus ( 0 < 1 / 2 & 1 / 2 < 1 ) ; :: thesis: for x, y being Point of M holds dist ((f . x),(f . y)) <= (1 / 2) * (dist (x,y))
let z, y be Point of M; :: thesis: dist ((f . z),(f . y)) <= (1 / 2) * (dist (z,y))
( f . z = the Point of M & f . y = the Point of M ) by FUNCOP_1:7;
then A1: dist ((f . z),(f . y)) = 0 by METRIC_1:1;
dist (z,y) >= 0 by METRIC_1:5;
hence dist ((f . z),(f . y)) <= (1 / 2) * (dist (z,y)) by A1; :: thesis: verum