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