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