set A = the Function of X,NAT;
A1: ( rng the Function of X,NAT c= REAL & dom the Function of X,NAT = X ) by VALUED_0:def 3, FUNCT_2:def 1;
reconsider A = the Function of X,NAT as Function of X,F_Real by A1, FUNCT_2:2;
A is natural-valued ;
hence ex b₁ being Function of X,F_Real st b₁ is natural-valued ; :: thesis: verum