let n be Element of NAT ; :: thesis: for A being non empty set
for f being Function of A,A
for x being Element of A holds (iter f,(n + 1)) . x = f . ((iter f,n) . x)
let A be non empty set ; :: thesis: for f being Function of A,A
for x being Element of A holds (iter f,(n + 1)) . x = f . ((iter f,n) . x)
let f be Function of A,A; :: thesis: for x being Element of A holds (iter f,(n + 1)) . x = f . ((iter f,n) . x)
let x be Element of A; :: thesis: (iter f,(n + 1)) . x = f . ((iter f,n) . x)
thus (iter f,(n + 1)) . x = (f * (iter f,n)) . x by FUNCT_7:73
.= f . ((iter f,n) . x) by FUNCT_2:21 ; :: thesis: verum