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