theorem Th7: :: ORDEQ_01:7

for X being RealBanachSpace
for f being Function of X,X st ex n0 being Nat st iter (f,n0) is contraction holds
f is with_unique_fixpoint