{} in {{} } * by FINSEQ_1:66;
then reconsider f = {} --> {} as Function of {} ,{{} } * by FUNCOP_1:58;
reconsider g = {} --> {} 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