let f be Function; :: thesis: iter (f,0) = id (field f)
ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( iter (f,0) = p . 0 & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = (p . k) * f ) ) by Def11;
hence iter (f,0) = id (field f) ; :: thesis: verum