{} 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: ( not ManySortedSign(# {{} },{{} },f,g #) is void & ManySortedSign(# {{} },{{} },f,g #) is strict & not ManySortedSign(# {{} },{{} },f,g #) is empty )
thus ( not ManySortedSign(# {{} },{{} },f,g #) is void & ManySortedSign(# {{} },{{} },f,g #) is strict & not ManySortedSign(# {{} },{{} },f,g #) is empty ) ; :: thesis: verum