:: deftheorem Def3 defines contraction NFCONT_2:def 3 :
for M being non empty NORMSTR
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).|| ) ) );