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