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