:: deftheorem Def1 defines contraction ALI2:def 1 :
for M being non empty MetrSpace
for f being Function of M,M holds
( f is contraction iff ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds dist ((f . x),(f . y)) <= L * (dist (x,y)) ) ) );