let m be Nat; :: thesis: for f being Function holds iter (f,m) c= f [*]
let f be Function; :: thesis: iter (f,m) c= f [*]

per cases ( m = 0 or m <> 0 ) ;

suppose m = 0 ; :: thesis: iter (f,m) c= f [*]

hence iter (f,m) c= f [*] by Lm31; :: thesis: verum

end;

suppose m <> 0 ; :: thesis: iter (f,m) c= f [*]

then consider n being Nat such that
A1: m = n + 1 by NAT_1:6;
thus iter (f,m) c= f [*] by Lm32, A1; :: thesis: verum

end;

end;