defpred S₁[ object , object ] means ex n being Nat st
( $2 = n & ( Im ((iter (O,n)),$1) <> {} or ( n = 0 & Im ((iter (O,n)),$1) = {} ) ) & Im ((iter (O,(n + 1))),$1) = {} );
A2: for x being object st x in X holds
ex y being object st
( y in NAT & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in X implies ex y being object st
( y in NAT & S₁[x,y] ) )
assume x in X ; :: thesis: ex y being object st
( y in NAT & S₁[x,y] )

per cases ( x nin field O or x in field O ) ;

suppose x nin field O ; :: thesis: ex y being object st
( y in NAT & S₁[x,y] )

then {x} /\ (field O) = {} by XBOOLE_0:def 7, ZFMISC_1:50;
then Im ((id (field O)),x) = {} by Th3;
then A3: Im ((iter (O,0)),x) = {} by FUNCT_7:68;
take y = 0 ; :: thesis: ( y in NAT & S₁[x,y] )
thus y in NAT ; :: thesis: S₁[x,y]
take n = 0 ; :: thesis: ( y = n & ( Im ((iter (O,n)),x) <> {} or ( n = 0 & Im ((iter (O,n)),x) = {} ) ) & Im ((iter (O,(n + 1))),x) = {} )
thus ( y = n & ( Im ((iter (O,n)),x) <> {} or ( n = 0 & Im ((iter (O,n)),x) = {} ) ) ) ; :: thesis: Im ((iter (O,(n + 1))),x) = {}
thus Im ((iter (O,(n + 1))),x) = Im (((iter (O,n)) * O),x) by FUNCT_7:71
.= O .: {} by A3, RELAT_1:126
.= {} ; :: thesis: verum

end;

suppose x in field O ; :: thesis: ex y being object st
( y in NAT & S₁[x,y] )

then {x} /\ (field O) = {x} by XBOOLE_1:28, ZFMISC_1:31;
then (id (field O)) .: {x} = {x} by Th3;
then A4: Im ((iter (O,0)),x) = {x} by FUNCT_7:68;
defpred S₂[ Nat] means (iter (O,$1)) .: {x} = {} ;
A5: ex n being Nat st S₂[n] by A1, Th20;
consider n being Nat such that
A6: ( S₂[n] & ( for k being Nat st S₂[k] holds
n <= k ) ) from NAT_1:sch 5(A5);
consider m being Nat such that
A7: n = m + 1 by A4, A6, NAT_1:6;
take y = m; :: thesis: ( y in NAT & S₁[x,y] )
thus y in NAT by ORDINAL1:def 12; :: thesis: S₁[x,y]
take m ; :: thesis: ( y = m & ( Im ((iter (O,m)),x) <> {} or ( m = 0 & Im ((iter (O,m)),x) = {} ) ) & Im ((iter (O,(m + 1))),x) = {} )
m < n by A7, NAT_1:13;
hence ( y = m & ( Im ((iter (O,m)),x) <> {} or ( m = 0 & Im ((iter (O,m)),x) = {} ) ) & Im ((iter (O,(m + 1))),x) = {} ) by A6, A7; :: thesis: verum

end;

end;

end;

consider f being Function such that
A8: ( dom f = X & rng f c= NAT & ( for x being object st x in X holds
S₁[x,f . x] ) ) from FUNCT_1:sch 6(A2);
reconsider f = f as Function of X,NAT by A8, FUNCT_2:2;
take R = value_of f; :: thesis: ex f being Function of X,NAT st
( R = value_of f & ( for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ) )
take f ; :: thesis: ( R = value_of f & ( for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ) )
thus R = value_of f ; :: thesis: for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} )
let x be Element of X; :: thesis: ( x in X implies ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) )
assume x in X ; :: thesis: ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} )
then consider n being Nat such that
A9: ( f . x = n & ( Im ((iter (O,n)),x) <> {} or ( n = 0 & Im ((iter (O,n)),x) = {} ) ) & Im ((iter (O,(n + 1))),x) = {} ) by A8;
take n ; :: thesis: ( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} )
thus ( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) by A9; :: thesis: verum