let X, x be set ; :: thesis: for n being Element of NAT
for f being Function of X,X st x is_a_fixpoint_of iter f,n holds
f . x is_a_fixpoint_of iter f,n
let n be Element of NAT ; :: thesis: for f being Function of X,X st x is_a_fixpoint_of iter f,n holds
f . x is_a_fixpoint_of iter f,n
let f be Function of X,X; :: thesis: ( x is_a_fixpoint_of iter f,n implies f . x is_a_fixpoint_of iter f,n )
assume A1: x is_a_fixpoint_of iter f,n ; :: thesis: f . x is_a_fixpoint_of iter f,n
then A2: x in dom (iter f,n) by ABIAN:def 3;
A3: dom f = X by FUNCT_2:67;
then ( dom (iter f,n) = X & f . x in rng f ) by A2, FUNCT_1:def 5, FUNCT_2:67;
hence f . x in dom (iter f,n) ; :: according to ABIAN:def 3 :: thesis: f . x = (iter f,n) . (f . x)
x = (iter f,n) . x by A1, ABIAN:def 3;
hence f . x = (f * (iter f,n)) . x by A2, FUNCT_1:23
.= (iter f,(n + 1)) . x by FUNCT_7:73
.= ((iter f,n) * f) . x by FUNCT_7:71
.= (iter f,n) . (f . x) by A2, A3, FUNCT_1:23 ;
:: thesis: verum