( dom (doms {} ) = {} " (SubFuncs {} ) & dom (rngs {} ) = {} " (SubFuncs {} ) ) by Def2, Def3, RELAT_1:60;
hence ( doms {} = {} & rngs {} = {} ) by RELAT_1:172; :: thesis: verum