defpred S₁[ set ] means $1 in X;
deffunc H₁( set ) -> set = r |^ (In $1,NAT );
deffunc H₂( set ) -> Element of NAT = 0 ;
A1: for a being set 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 Function of NAT ,REAL such that
A2: for a being set 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 natural number holds
( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) )
let i be natural number ; :: thesis: ( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) )
i in NAT by ORDINAL1:def 13;
then In i,NAT = i by FUNCT_7:def 1;
hence ( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) ) by A2; :: thesis: verum