let n be 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:71
.= f . ((iter (f,n)) . x) by FUNCT_2:15 ; :: thesis: verum