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