set f = X --> 0;
reconsider f = X --> 0 as ManySortedSet of X ;
take f ; :: thesis: f is natural-valued
thus f is natural-valued ; :: thesis: verum