set f = X --> 0 ;
dom (X --> 0 ) = X by FUNCOP_1:19;
then reconsider f = X --> 0 as ManySortedSet of by PARTFUN1:def 4;
take f ; :: thesis: f is natural-valued
thus f is natural-valued ; :: thesis: verum