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