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 :: thesis: for x being object st x in union { (iter (f,mm)) where mm is Element of NAT : verum } holds
x in f [*]
let x be object ; :: 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
A1: ( 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
A2: X = iter (f,mm) by A1;
( x in iter (f,mm) & iter (f,mm) c= f [*] ) by A1, A2, Lm33;
hence x in f [*] ; :: thesis: verum
end;
then A3: union { (iter (f,mm)) where mm is Element of NAT : verum } c= f [*] ;
assume A4: rng f c= dom f ; :: thesis: f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum }
now :: thesis: for x being object st x in f [*] holds
x in union { (iter (f,mm)) where mm is Element of NAT : verum }
let x be object ; :: 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
A5: x in iter (f,m) by A4, Lm36;
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 A5;
hence x in union { (iter (f,mm)) where mm is Element of NAT : verum } by TARSKI:def 4; :: thesis: verum
end;
then A6: f [*] c= union { (iter (f,mm)) where mm is Element of NAT : verum } ;
thus f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } by A3, A6; :: thesis: verum