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