let X be 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 ) )
let f be Function of X,X; ( ex n0 being Element of NAT st iter (f,n0) is Contraction of X implies ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) ) )
given n0 being Element of NAT such that A1:
iter (f,n0) is Contraction of X
; ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
consider xp being Point of X such that
A2:
(iter (f,n0)) . xp = xp
and
A3:
for x being Point of X st (iter (f,n0)) . x = x holds
xp = x
by A1, Th40;
A4:
now for x being Point of X st f . x = x holds
xp = xlet x be
Point of
X;
( f . x = x implies xp = x )assume A5:
f . x = x
;
xp = x
for
n being
Element of
NAT holds
(iter (f,n)) . x = x
then
(iter (f,n0)) . x = x
;
hence
xp = x
by A3;
verum end;
A10:
iter (f,n0) is Function of X,X
by FUNCT_7:83;
(iter (f,n0)) . (f . xp) =
((iter (f,n0)) * f) . xp
by FUNCT_2:15
.=
(iter (f,(n0 + 1))) . xp
by FUNCT_7:69
.=
(f * (iter (f,n0))) . xp
by FUNCT_7:71
.=
f . xp
by A2, A10, FUNCT_2:15
;
then
f . xp = xp
by A3;
hence
ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
by A4; verum