theorem :: FOMODEL0:18

for g being Function
for m being Nat
for f being Function st f c= g holds
iter (f,m) c= iter (g,m) by Lm26;