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