theorem :: FOMODEL0:17

for f being Function st rng f c= dom f holds
f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } by Lm37;