deffunc H₁( object ) -> Element of omega = 0 ;
deffunc H₂( object ) -> set = r |^ (In ($1,NAT));
defpred S₁[ object ] means $1 in X;
A1: for a being object st a in NAT holds
( ( S₁[a] implies H₂(a) in REAL ) & ( not S₁[a] implies H₁(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₁[a] implies f . a = H₂(a) ) & ( not S₁[a] implies f . a = H₁(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