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