theorem :: FUNCT_6:23

( doms {} = {} & rngs {} = {} ) by Def1, Def2, RELAT_1:38;