:: deftheorem Def7 defines contraction NCFCONT2:def 7 :
for M being non empty CNORMSTR
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 ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) ) );