for X being ComplexBanachSpace
for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is Contraction of X holds
ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )