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