deffunc H_{1}( object ) -> Element of omega = 0 ;

deffunc H_{2}( object ) -> set = r |^ (In ($1,NAT));

defpred S_{1}[ object ] means $1 in X;

A1: for a being object st a in NAT holds

( ( S_{1}[a] implies H_{2}(a) in REAL ) & ( not S_{1}[a] implies H_{1}(a) in REAL ) )
by XREAL_0:def 1;

consider f being sequence of REAL such that

A2: for a being object st a in NAT holds

( ( S_{1}[a] implies f . a = H_{2}(a) ) & ( not S_{1}[a] implies f . a = H_{1}(a) ) )
from FUNCT_2:sch 5(A1);

take f ; :: thesis: for i being Nat holds

( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) )

let i be Nat; :: thesis: ( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) )

In (i,NAT) = i ;

hence ( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) ) by A2; :: thesis: verum

deffunc H

defpred S

A1: for a being object st a in NAT holds

( ( S

consider f being sequence of REAL such that

A2: for a being object st a in NAT holds

( ( S

take f ; :: thesis: for i being Nat holds

( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) )

let i be Nat; :: thesis: ( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) )

In (i,NAT) = i ;

hence ( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) ) by A2; :: thesis: verum