let f be Function; :: thesis: for n being Nat holds iter (f,(n + 1)) = (iter (f,n)) * f
let n be Nat; :: thesis: iter (f,(n + 1)) = (iter (f,n)) * f
consider p being Function of NAT,(PFuncs ((field f),(field f))) such that
A1: ( p . (n + 1) = iter (f,(n + 1)) & p . 0 = id (field f) ) and
A2: for k being Nat holds p . (k + 1) = (p . k) * f by Def11;
p . (n + 1) = (p . n) * f by A2;
hence iter (f,(n + 1)) = (iter (f,n)) * f by A1, A2, Def11; :: thesis: verum