reconsider g = {} --> {} as Function of {},{{}} ;
reconsider f = {} --> {} as Function of {},({{}} *) ;
take ManySortedSign(# {{}},{},f,g #) ; :: thesis: ( ManySortedSign(# {{}},{},f,g #) is void & ManySortedSign(# {{}},{},f,g #) is strict & not ManySortedSign(# {{}},{},f,g #) is empty )
thus ( ManySortedSign(# {{}},{},f,g #) is void & ManySortedSign(# {{}},{},f,g #) is strict & not ManySortedSign(# {{}},{},f,g #) is empty ) ; :: thesis: verum