let f be Function; :: thesis: iter (f,0) c= f [*]
set LH = iter (f,0);
set RH = f [*] ;
iter (f,0) = id (field f) by FUNCT_7:68
.= id (field (f [*])) by Lm30 ;
hence iter (f,0) c= f [*] by RELAT_2:1; :: thesis: verum