consider a being Function of {},({x} *);
consider r being Function of {},{x};
reconsider S = ManySortedSign(# {x},{},a,r #) as void strict ManySortedSign ;
take S ; :: thesis: the carrier of S = {x}
thus the carrier of S = {x} ; :: thesis: verum