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)) ;
A3: dom f = X by FUNCT_2:52;
then ( dom (iter (f,n)) = X & f . x in rng f ) by A2, FUNCT_1:def 3, FUNCT_2:52;
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;
hence f . x = (f * (iter (f,n))) . x by A2, FUNCT_1:13
.= (iter (f,(n + 1))) . x by FUNCT_7:71
.= ((iter (f,n)) * f) . x by FUNCT_7:69
.= (iter (f,n)) . (f . x) by A2, A3, FUNCT_1:13 ;
:: thesis: verum