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