let f be Function; :: thesis: for n being Element of NAT holds (id ((dom f) \/ (rng f))) * (iter (f,n)) = iter (f,n)
let n be Element of NAT ; :: thesis: (id ((dom f) \/ (rng f))) * (iter (f,n)) = iter (f,n)
rng (iter (f,n)) c= (dom f) \/ (rng f) by Th74;
hence (id ((dom f) \/ (rng f))) * (iter (f,n)) = iter (f,n) by RELAT_1:79; :: thesis: verum