let f be Function of M,M; :: thesis: ( f is constant implies f is contraction )

assume A1: f is constant ; :: 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))

dom f = the carrier of M by FUNCT_2:def 1;

then f . z = f . y by A1, FUNCT_1:def 10;

then A2: 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 A2; :: thesis: verum

assume A1: f is constant ; :: 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))

dom f = the carrier of M by FUNCT_2:def 1;

then f . z = f . y by A1, FUNCT_1:def 10;

then A2: 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 A2; :: thesis: verum