{} in {} * by FINSEQ_1:66;
then reconsider f = {} --> {} as Function of {} ,{} * by FUNCOP_1:58;
( dom ({} --> {} ) = {} & rng ({} --> {} ) = {} ) ;
then reconsider g = {} --> {} as Function of {} , {} by FUNCT_2:def 1, RELSET_1:11;
take ManySortedSign(# {} ,{} ,f,g #) ; :: thesis: ( ManySortedSign(# {} ,{} ,f,g #) is empty & ManySortedSign(# {} ,{} ,f,g #) is void )
thus ( ManySortedSign(# {} ,{} ,f,g #) is empty & ManySortedSign(# {} ,{} ,f,g #) is void ) ; :: thesis: verum