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;