{} in {{}} * by FINSEQ_1:49;
then reconsider f = {{}} --> {} as Function of {{}},({{}} *) by FUNCOP_1:46;
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