theorem FIXPOINT: :: NDIFF_8:28

for X being RealBanachSpace
for S being non empty Subset of X
for f being PartFunc of X,X st S is closed & dom f = S & rng f c= S & ex k being Real st
( 0 < k & k < 1 & ( for x, y being Point of X st x in S & y in S holds
||.((f /. x) - (f /. y)).|| <= k * ||.(x - y).|| ) ) holds
( ex x0 being Point of X st
( x0 in S & f . x0 = x0 ) & ( for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds
x0 = y0 ) )