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
reconsider n = n as Element of NAT by ORDINAL1:def 13;
consider p being Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))) such that
A1: ( p . (n + 1) = iter f,(n + 1) & p . 0 = id ((dom f) \/ (rng f)) ) and
A2: for k being Nat ex g being Function st
( g = p . k & p . (k + 1) = g * f ) by Def11;
ex g being Function st
( g = p . n & p . (n + 1) = g * f ) by A2;
hence iter f,(n + 1) = (iter f,n) * f by A1, A2, Def11; :: thesis: verum