let f be Function; :: thesis: ( rng f c= dom f implies f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } )
set F = { (iter (f,mm)) where mm is Element of NAT : verum } ;
set LH = f [*] ;
set RH = union { (iter (f,mm)) where mm is Element of NAT : verum } ;

now

let x be set ; :: thesis: ( x in union { (iter (f,mm)) where mm is Element of NAT : verum } implies x in f [*] )
assume x in union { (iter (f,mm)) where mm is Element of NAT : verum } ; :: thesis: x in f [*]
then consider X being set such that
C0: ( x in X & X in { (iter (f,mm)) where mm is Element of NAT : verum } ) by TARSKI:def 4;
consider mm being Element of NAT such that
C1: X = iter (f,mm) by C0;
( x in iter (f,mm) & iter (f,mm) c= f [*] ) by C0, C1, Lm40;
hence x in f [*] ; :: thesis: verum

end;

then B1: union { (iter (f,mm)) where mm is Element of NAT : verum } c= f [*] by TARSKI:def 3;
assume B0: rng f c= dom f ; :: thesis: f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum }

now

let x be set ; :: thesis: ( x in f [*] implies x in union { (iter (f,mm)) where mm is Element of NAT : verum } )
assume x in f [*] ; :: thesis: x in union { (iter (f,mm)) where mm is Element of NAT : verum }
then consider m being Nat such that
C0: x in iter (f,m) by B0, Lm41;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
( x in iter (f,mm) & iter (f,mm) in { (iter (f,mm)) where mm is Element of NAT : verum } ) by C0;
hence x in union { (iter (f,mm)) where mm is Element of NAT : verum } by TARSKI:def 4; :: thesis: verum

end;

then B2: f [*] c= union { (iter (f,mm)) where mm is Element of NAT : verum } by TARSKI:def 3;
thus f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } by B1, B2, XBOOLE_0:def 10; :: thesis: verum