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