not dom G is empty ;
then reconsider f = rngs G as non empty non-empty Function by FUNCT_6:90, RELAT_1:60;
not Union f is empty ;
hence not Values G is empty by GOBRD13:def 1; :: thesis: verum