( dom ({} --> {}) = {} & rng ({} --> {}) = {} ) ;
then reconsider g = {} --> {} as Function of {},{} by RELSET_1:4;
{} in {} * by FINSEQ_1:49;
then reconsider f = {} --> {} as Function of {},({} *) by FUNCOP_1:46;
take ManySortedSign(# {},{},f,g #) ; :: thesis: ( ManySortedSign(# {},{},f,g #) is strict & ManySortedSign(# {},{},f,g #) is empty & ManySortedSign(# {},{},f,g #) is void )
thus ( ManySortedSign(# {},{},f,g #) is strict & ManySortedSign(# {},{},f,g #) is empty & ManySortedSign(# {},{},f,g #) is void ) ; :: thesis: verum