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